First-order logic is a formal system for expressing statements about objects and their relationships. It extends propositional logic by introducing variables, quantifiers and predicates so that one can say not only that propositions are true or false, but that properties hold of individual elements of a domain. For a short technical introduction see basic overview, and for applications in mathematics and philosophy consult mathematical uses and philosophical uses.
Basic syntax and components
The language of first-order logic is built from a few kinds of symbols combined by clear formation rules. Atomic parts include constant symbols (names for specific elements), variables, function symbols (that return elements), and predicate symbols (that return truth values). These are assembled into terms and then into atomic formulas by applying predicates to terms. A formal grammar and set of formation rules is often presented separately; see a short guide to syntax at syntax notes. First-order logic also contains the usual Boolean connectives shared with propositional logic; compare with propositional logic.
Quantifiers, connectives and examples
Two quantifiers let the language talk about many objects: the universal quantifier (written with the symbol shown here) ∀ expresses that a property holds for every element of the domain, while the existential quantifier ∃ asserts that some element has the property. Negation, conjunction, disjunction and implication combine quantified formulas much as they do in propositional logic; an accessible account of quantifier rules is available at quantifier primer. Semantically, a sentence like "∀x P(x) → ∃y Q(y)" is evaluated by interpreting predicate symbols and functions in a particular structure; more about semantic evaluation can be found at semantics.
Semantics, models and interpretation
Meaning in first-order logic is given by structures or models: a domain of discourse together with interpretations of the nonlogical symbols. A sentence is true in a structure if the usual recursive rules assign it truth given that interpretation. Model-theoretic notions such as satisfiability, validity and entailment are central: a sentence is satisfiable if some model makes it true; it is valid if every model does. Introductory model theory resources include model theory and examples.
Key metatheorems and limitations
Several general results explain the power and boundaries of first-order logic. Gödel's completeness theorem establishes that a formula is semantically valid exactly when it has a formal proof in a suitable deductive system. The compactness theorem and the Löwenheim–Skolem theorems describe remarkable consequences for the sizes of models and for transfer of truth between finite and infinite contexts. At the same time, Church and Turing showed that first-order logic is undecidable in general: there is no algorithm that decides validity for every sentence. For formal statements and proofs see completeness and decidability.
History, role and applications
Developed in the late nineteenth and early twentieth centuries as part of the formalization of mathematics and logic, first-order logic became the standard framework for much of modern mathematics and for formal theories such as set theory (for example, Zermelo–Fraenkel set theory is usually formulated in first-order logic). It underpins areas as diverse as model theory, proof theory, database theory, and parts of computer science; introductory surveys and applications are collected at further reading.
Distinguished from more expressive systems (such as second-order logic), first-order logic strikes a balance: it is expressive enough to formalize large parts of mathematics while possessing powerful general metatheorems, yet it cannot capture some properties (like finiteness) in a single first-order sentence. These trade-offs shape its central place in logic and foundations.