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").

Semantics

A structure (model) M = a domain set + interpretations of the constant/function/predicate symbols. Satisfaction M ⊨ φ says "φ is true in M." 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.