First-order logic (FOL)
Parent: logic
The standard logic of mathematics: quantify over elements of a domain (not over sets — that's second-order / MSO).
Syntax
- Terms: variables, constants, and function symbols applied to terms (
f(x, c)).- Atomic formulas: a predicate applied to terms (
P(x),x = y,x < y).- Formulas: atoms closed under
¬, ∧, ∨, →and the quantifiers∀x("for all elements"),∃x("for some element").
SemanticsA structure (model)
M= a domain set + interpretations of the constant/function/predicate symbols. SatisfactionM ⊨ φsays "φis true inM." A sentence is valid if true in every model (⊨ φ), satisfiable if true in some, andΓ ⊨ φ(entailment) if every model ofΓsatisfiesφ.
The two great theorems
- Gödel's completeness theorem (1929): there is a sound and complete proof system —
⊢ φ ⟺ ⊨ φ(provable = valid). (Don't confuse with incompleteness: completeness is about FOL validity; incompleteness is about specific theories like arithmetic being unable to prove all truths.) - Compactness: if every finite subset of
Γis satisfiable, thenΓis satisfiable. A workhorse of model theory (builds infinite/non-standard models).
The catch
Completeness makes validity semi-decidable — enumerate proofs and you'll find one iff φ is valid. But you cannot decide validity in general: that's the undecidability of FOL (the Entscheidungsproblem), and it's exactly what Turing's 1936 paper was built to settle.