First-Order Logic

Origin. Gottlob Frege's Begriffsschrift (1879) introduced quantification over individuals. Charles Sanders Peirce independently developed quantification (1885). Giuseppe Peano developed logical notation (1889). Bertrand Russell and Alfred North Whitehead systematized it in Principia Mathematica (1910-1913). Also called predicate logic, predicate calculus, or quantificational logic. The standard logic of mathematics and formal verification.

Models. Properties of individuals and relations between them. Quantification: "for all x" and "there exists x." Internal structure of propositions: "Socrates is mortal" becomes Mortal(socrates), allowing inference to "something is mortal." The logic of predicates, functions, and quantifiers over a domain of individuals.

Formalism.

Syntax:

• Terms: variables (x, y, ...), constants (a, b, ...), functions (f(t₁,...,tₙ))
• Atomic formulas: P(t₁,...,tₙ) where P is a predicate and tᵢ are terms
• Formulas: atomic formulas closed under ¬, ∧, ∨, →, ↔, ∀x, ∃x

Semantics: A structure M = (D, I) where:

• D is a non-empty domain (universe of discourse)
• I interprets constants as elements, functions as functions on D, predicates as relations on D

Truth in a structure under variable assignment:

• M, σ ⊨ P(t₁,...,tₙ) iff (⟦t₁⟧σ, ..., ⟦tₙ⟧σ) ∈ I(P)
• M, σ ⊨ ∀xφ iff for all d ∈ D, M, σ[x↦d] ⊨ φ
• M, σ ⊨ ∃xφ iff for some d ∈ D, M, σ[x↦d] ⊨ φ

Validity: φ is valid iff true in all structures. φ entails ψ iff every structure satisfying φ satisfies ψ.

Hilbert axioms (quantifier fragment): ∀x.φ → φ[t/x] (instantiation, t free for x) ∀x.(φ → ψ) → (∀x.φ → ∀x.ψ) (distribution) Rules: modus ponens; generalization (from φ infer ∀x.φ, x not free in open assumptions).

Proof systems: Natural deduction, sequent calculus, Hilbert systems, resolution. Quantifier rules: ∀-elimination (instantiate), ∃-introduction (witness), ∀-introduction (generalize with fresh variable), ∃-elimination (assume witness).

Symbols.

Metatheory. Gödel's completeness theorem (1930) is the founding result: a sentence is derivable in the standard calculus exactly when it is true in every structure, so ⊢ and ⊨ coincide and the valid sentences are recursively enumerable. Compactness and the Löwenheim–Skolem theorems fall out of it — a theory all of whose finite subsets are satisfiable is satisfiable, and a theory with an infinite model has models of every infinite cardinality at or above the size of its language — and Henkin's 1949 proof derives all three from one construction. Validity is nonetheless undecidable, by Church and Turing independently in 1936, so the logic is semi-decidable and no more; Trakhtenbrot (1950) showed that validity over finite models is not even semi-decidable, so the two directions fail in opposite ways. Craig interpolation (1957) holds, and Beth definability follows from it: implicit definability implies explicit definability. Lindström (1969) proved these results characterize the logic — any abstract logic with compactness and downward Löwenheim–Skolem that extends first-order logic is equivalent to it — so the whole package is not a set of accidents but a maximum.

Applies to. Mathematics (formalization of proofs). Databases (query languages, integrity constraints). Formal verification. Knowledge representation. Foundations of computer science. Any domain requiring precise reasoning about objects and their properties.

Limitations. Validity is undecidable (Church and Turing, 1936) and only semi-decidable: the valid formulas can be enumerated, the invalid ones cannot, so a failed proof search is uninformative. Over finite models the situation is worse — Trakhtenbrot (1950) showed finite validity is not even recursively enumerable, so finite model theory has no completeness theorem at all. Expressively, compactness and Löwenheim–Skolem together forbid categoricity: any theory with an infinite model has models of every infinite cardinality, so ℕ, ℝ and the well-orderings cannot be characterized up to isomorphism and non-standard models are unavoidable rather than pathological. Finiteness, countability, transitive closure, reachability, well-foundedness, equicardinality and "most" are all inexpressible. None of this can be repaired by a better-designed logic: Lindström's theorem (1969) says first-order logic is already the strongest logic having both compactness and downward Löwenheim–Skolem, so every gain in expressive power costs one of them. The logic is purely extensional, so modal, temporal and attitude contexts fall outside it, and the standard semantics requires a non-empty domain, which is why empty models need inclusive or free logic.

© 2026 Lingenic LLC