First-Order Logic (FOL), also called predicate logic, is a formal system that extends propositional logic with quantifiers, variables, predicates and functions, allowing statements about objects and their relationships. It can express assertions such as “every X has some Y” through universal and existential quantification over a domain of discourse. FOL provides a precise syntax and model-theoretic semantics that underpin automated reasoning, knowledge representation and the foundations of mathematics.
Overview
- FOL formalises reasoning by combining terms (constants, variables and functions) into atomic formulae using predicates, then composing them with logical connectives and the quantifiers for-all and there-exists. Its semantics is given by interpretations that assign meanings to symbols over a domain; a sentence is valid if true in every interpretation. Although FOL is semi-decidable, it is expressive enough to capture much of mathematics and serves as the target language for many knowledge-representation systems.
Mechanisms
- Syntax — terms, predicates, connectives and the universal and existential quantifiers.
- Model-theoretic semantics — interpretations over a domain of discourse fix truth values.
- Inference rules — modus ponens, resolution and unification derive entailed sentences.
- Soundness and completeness — derivations preserve truth and capture all valid entailments.
- Decidability limits — validity is semi-decidable; satisfiability is undecidable in general.
Applications
- Automated theorem provers and proof assistants.
- Knowledge bases and rule engines in symbolic AI.
- Formal specification and verification of software and hardware.
- Foundations for ontologies and the semantic web.