# 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.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| ∀ | U+2200 | Universal quantifier | For all |
| ∃ | U+2203 | Existential quantifier | There exists |
| ∄ | U+2204 | Negated existential | There does not exist |
| = | — | Equality | Identity of individuals |
| ≠ | U+2260 | Inequality | Distinct individuals |
| ¬ ∧ ∨ → ↔ | — | Connectives | (as in propositional) |
| ⊨ | U+22A8 | Entailment | Semantic consequence |
| ⊢ | U+22A2 | Derives | Syntactic derivation |
| ∈ | U+2208 | Element | Domain membership |
| D | — | Domain | Universe of discourse |

**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