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): a formula is provable iff valid — syntax matches semantics. Compactness: if every finite subset of a theory is satisfiable, the whole theory is. Löwenheim-Skolem: if a theory has an infinite model, it has models of every infinite cardinality. Undecidability (Church, Turing 1936): validity is undecidable — no algorithm determines whether an arbitrary formula is valid. Semi-decidable: valid formulas can be enumerated. First-order logic cannot characterize the natural numbers up to isomorphism (non-categoricity).

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. Undecidable: no algorithm for validity. Cannot express "finitely many," transitive closure, or well-foundedness. Löwenheim-Skolem implies no categorical axiomatization of infinite structures. Second-order properties (like "is finite") require second-order logic. Equality can be included or excluded; with equality, some additional complexity. Cannot express everything needed for arithmetic (Gödel incompleteness applies to sufficiently strong first-order theories).

© 2026 Lingenic LLC