First-order logic (FOL), also known as predicate logic, is a formal system in mathematical logic that extends propositional logic by incorporating quantifiers (∀ "for all," ∃ "there exists") and predicates that express properties of objects or relations among them. It provides a precise language for representing statements about individual objects and their relationships, forming the foundation for much of modern mathematics, computer science (especially automated reasoning and database theory), and analytic philosophy.

1 Syntax

The syntax of first-order logic defines the well‑formed expressions (formulas) of the language. It consists of an alphabet and a set of formation rules.

1.1 Alphabet of first‑order logic

The alphabet is divided into logical symbols and non‑logical symbols.

1.1.1 Logical symbols

The logical symbols are fixed and have a constant meaning across all first‑order languages. They include:

  • Connectives: ¬ (negation), ∧ (conjunction), ∨ (disjunction), → (implication), ↔ (biconditional).
  • Quantifiers: ∀ (universal quantifier, “for all”), ∃ (existential quantifier, “there exists”).
  • Variables: typically denoted by letters such as x, y, z, possibly with subscripts.
  • Equality: the binary predicate symbol = (although sometimes treated as a logical symbol, in some treatments it is included in the non‑logical part).
  • Punctuation: parentheses and commas.

1.1.2 Non‑logical symbols

The non‑logical symbols form the signature of a particular first‑order language. They include:

  • Constant symbols: names for specific individuals (e.g., a, b, c).
  • Function symbols: symbols that denote functions from individuals to individuals, each with a fixed arity (e.g., f, g).
  • Predicate symbols: symbols that denote properties or relations among individuals, each with a fixed arity (e.g., P, Q, R). The equality symbol is often considered a distinguished binary predicate.

1.2 Terms

Terms are the syntactic expressions that refer to objects. They are defined recursively:

  • Every variable or constant symbol is a term.
  • If f is an n‑ary function symbol and t₁, …, tₙ are terms, then f(t₁, …, tₙ) is a term.

No other expressions are terms.

1.3 Formulas

Formulas are statements that can be true or false. They are built from atomic formulas using connectives and quantifiers.

1.3.1 Atomic formulas

An atomic formula is an expression of the form P(t₁, …, tₙ) where P is an n‑ary predicate symbol and t₁, …, tₙ are terms. If equality is included, then t₁ = t₂ is also an atomic formula.

1.3.2 Compound formulas

Compound formulas are formed by applying logical connectives to formulas:

  • If φ is a formula, then ¬φ is a formula.
  • If φ and ψ are formulas, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are formulas.

1.3.3 Quantified formulas

If φ is a formula and x is a variable, then ∀x φ and ∃x φ are formulas. The variable x is said to be bound by the quantifier.

1.3.4 Binding and scope of variables

The scope of a quantifier is the subformula to which it applies. An occurrence of a variable in a formula is bound if it lies within the scope of a quantifier over that variable; otherwise it is free. A formula with no free variables is called a sentence. The same variable may occur both free and bound in different places, though such usage is often avoided in standard practice.

2 Semantics

Semantics assigns meaning to the syntactic expressions by specifying a domain of discourse and interpreting the non‑logical symbols.

2.1 Structures and interpretations

A first‑order structure (or model) for a given signature consists of:

  • A non‑empty set M, the domain or universe of discourse.
  • For each constant symbol c, an element cᴹ ∈ M.
  • For each n‑ary function symbol f, a function fᴹ: Mⁿ → M.
  • For each n‑ary predicate symbol P (excluding equality), a subset Pᴹ ⊆ Mⁿ, representing the tuples for which the predicate holds.

An interpretation (or valuation) of variables is a function s from the set of variables to M. Terms are evaluated recursively in the obvious way: the value of a constant is its interpretation, the value of a variable is given by s, and the value of a function term is computed by applying the interpreted function.

2.2 Satisfaction and truth

A formula φ is said to be satisfied in a structure M under a variable assignment s (written M ⊧ φ[s]) according to the following inductive definition:

  • M ⊧ P(t₁, …, tₙ)[s] iff (value(t₁), …, value(tₙ)) ∈ Pᴹ.
  • M ⊧ t₁ = t₂[s] iff value(t₁) = value(t₂).
  • M ⊧ ¬φ[s] iff not M ⊧ φ[s].
  • M ⊧ (φ ∧ ψ)[s] iff M ⊧ φ[s] and M ⊧ ψ[s] (similarly for other connectives).
  • M ⊧ ∀x φ[s] iff for every element a ∈ M, M ⊧ φ[s(x/a)], where s(x/a) is the assignment that maps x to a and agrees with s elsewhere.
  • M ⊧ ∃x φ[s] iff there exists an element a ∈ M such that M ⊧ φ[s(x/a)].

2.2.1 Truth conditions for quantifiers

The truth conditions for quantifiers capture the intuitive meaning of “for all” and “there exists”: ∀x φ is true if φ holds for every value of x in the domain; ∃x φ is true if φ holds for at least one value of x. The satisfaction of a sentence (a formula with no free variables) does not depend on the variable assignment; we then say that M is a model of the sentence.

2.3 Validity, satisfiability, and logical consequence

A formula φ is valid (or logically true) if it is satisfied in every structure under every variable assignment (i.e., ⊧ φ). A formula is satisfiable if there exists some structure and assignment that satisfies it. A sentence φ is a logical consequence of a set of sentences Γ (written Γ ⊧ φ) if every structure that satisfies all sentences in Γ also satisfies φ.

3 Proof Theory

Proof theory studies syntactic methods for deriving formulas from axioms using inference rules. Several proof systems for first‑order logic have been developed, all of which are equivalent in their deductive power.

3.1 Hilbert‑style axiomatic systems

Hilbert‑style systems consist of a finite set of axiom schemas and a single inference rule (typically modus ponens). Axiom schemas cover the classical propositional tautologies and the quantifier axioms, such as:

  • ∀x φ → φ[t/x] (where t is a term free for x in φ).
  • ∀x (φ → ψ) → (φ → ∀x ψ) (with x not free in φ).

Proofs are sequences of formulas each of which is either an axiom or derived by modus ponens from earlier formulas. Such systems are convenient for metamathematical studies but impractical for actual deduction.

3.2 Natural deduction

Natural deduction, introduced by Gentzen, aims to mimic natural reasoning. It has introduction and elimination rules for each connective and quantifier. For example, the ∀‑introduction rule allows one to infer ∀x φ from φ provided the variable x does not occur free in any open assumptions. The ∀‑elimination rule deduces φ[t/x] from ∀x φ. Natural deduction is widely used in proof assistants and logic courses.

3.3 Sequent calculus

Also due to Gentzen, the sequent calculus works with sequents of the form Γ ⇒ Δ, where Γ and Δ are finite lists of formulas. Rules manipulate both sides of the sequent. The cut‑elimination theorem (Hauptsatz) shows that any proof can be transformed into one without the cut rule, yielding important structural properties.

3.4 Soundness and completeness theorems

Soundness states that every formula provable in a proof system is valid (i.e., true in all structures). Completeness (proved by Kurt Gödel in 1929) states that every valid formula is provable. For first‑order logic with equality, the completeness theorem holds: Γ ⊧ φ if and only if Γ ⊢ φ (in any standard proof system). This result establishes the perfect alignment between semantic truth and syntactic provability.

4 Model Theory

Model theory investigates the relationship between first‑order languages and their interpretations (models). It concerns the classification of models according to their structural properties.

4.1 Compactness theorem

The compactness theorem states that a set of first‑order sentences has a model if and only if every finite subset of it has a model. This powerful result follows easily from the completeness theorem (or can be proved independently). It has many consequences, such as the existence of non‑standard models of arithmetic.

4.2 Löwenheim–Skolem theorems

The Löwenheim–Skolem theorems relate the cardinality of a model to the size of the language.

4.2.1 Upward and downward versions

  • Downward Löwenheim–Skolem: If a countable set of sentences has an infinite model, then it has a model of every infinite cardinality greater than or equal to the cardinality of the language (usually countable). In particular, it has a countable model.
  • Upward Löwenheim–Skolem: If a countable set of sentences has an infinite model, then it has models of every infinite cardinality.

These results highlight the limitations of first‑order logic in fixing the size of the domain.

4.3 Elementary equivalence and substructures

Two structures M and N for the same signature are elementarily equivalent if they satisfy exactly the same first‑order sentences. A substructure N of M is elementary if for every first‑order formula φ(x₁, …, xₙ) and every tuple a from N, N ⊧ φ[a] iff M ⊧ φ[a]. The concept of elementary substructures is central to model theory and is used in tools such as the elementary chain theorem.

5 Properties and Limitations

First‑order logic, while powerful, has inherent limitations.

5.1 Decidability and undecidability

The decision problem for first‑order logic asks whether there is an algorithm that, given a formula, determines its validity. This problem is undecidable.

5.1.1 Church's theorem

Alonzo Church (1936) proved that first‑order logic is undecidable: no algorithm exists that, for every formula, correctly decides whether it is valid. This result is equivalent to the unsolvability of the Entscheidungsproblem. However, validity is recursively enumerable (there is a semi‑decision procedure), thanks to the completeness theorem.

5.2 Expressive power compared to propositional logic

Propositional logic can only express Boolean combinations of atomic propositions, whereas first‑order logic can quantify over individuals. This allows the formalization of statements such as “every number has a successor” or “there is a person who loves all numbers.” The expressive power is vastly greater.

5.2.1 Limits of first‑order logic

Despite its strength, first‑order logic cannot express properties that require quantification over relations or sets of individuals. For example, the property of finiteness (“the domain is finite”) or connectedness in a graph cannot be expressed by any set of first‑order sentences (compactness and Löwenheim–Skolem show this). Also, arithmetic truth is not first‑order definable, as shown by Gödel's incompleteness theorems.

5.3 Gödel's incompleteness theorems (relevance)

Gödel's incompleteness theorems apply to sufficiently strong axiomatic systems (e.g., Peano arithmetic) that are formalizable in first‑order logic. The first theorem states that any consistent, recursively enumerable extension of arithmetic is incomplete (there are true sentences that cannot be proved). The second theorem says that such a system cannot prove its own consistency. These results reveal deep limitations of first‑order axiomatizations of mathematics.

6 Applications

First‑order logic is widely used across many fields.

6.1 Mathematics

First‑order logic provides a rigorous framework for axiomatizing mathematical theories, including group theory, ring theory, and the theory of ordered fields.

6.1.1 Formalization of set theory

The most common foundational system, Zermelo‑Fraenkel set theory (ZFC), is expressed as a first‑order theory. The language includes a single binary predicate ∈, and all mathematical objects are treated as sets. Though unrestricted comprehension leads to paradoxes, ZFC’s axioms suffice to derive most of classical mathematics.

6.2 Computer science

6.2.1 Automated theorem proving

First‑order logic is the basis for many automated theorem provers (e.g., E, Vampire, Prover9). The resolution principle (developed by John Alan Robinson) provides a refutation‑complete method for first‑order logic, powering many proof‑search algorithms.

6.2.2 Knowledge representation and logic programming

Logic programming languages such as Prolog are based on a subset of first‑order logic (Horn clauses). Facts and rules are written as first‑order sentences, and queries are answered via resolution. This approach supports deductive databases and natural language processing.

6.2.3 Database query languages (SQL roots)

The relational database model owes much to first‑order logic. Relational calculus, a precursor to SQL, is based on first‑order predicate logic. SQL’s SELECT...FROM...WHERE clauses correspond to safe first‑order queries, including quantifier‑like constructs (EXISTS, NOT EXISTS).

6.3 Philosophy

6.3.1 Ontology and logical analysis

Analytic philosophers use first‑order logic to analyze the logical form of natural language sentences, clarify ontological commitments, and formalize metaphysical arguments. For example, Bertrand Russell’s theory of descriptions expresses “The present king of France is bald” as a conjunction of existential and universal statements, avoiding reference to non‑existent entities. First‑order logic remains a core tool in formal ontology and the philosophy of language.