First-order logic

Builds on

Required prerequisites, all the way down: 5

You will learn to

• Write first-order formulas in a given signature, such as the axioms for groups or for linear orders.
• Decide whether a sentence is true in a given structure by unwinding the definition of satisfaction.
• Prove soundness for a natural-deduction system and state Gödel's completeness theorem.

Definition

• A signature specifies constant, function and relation symbols, each with an arity.
• A structure for a signature is a non-empty set together with interpretations of its symbols.
• M ⊨ φ means the sentence φ is true in M; Γ ⊨ φ means φ is true in every model of Γ.
• Γ ⊢ φ means φ is derivable from Γ in a fixed proof system.

Theorem

• Soundness: if Γ ⊢ φ then Γ ⊨ φ.
• Isomorphic structures satisfy exactly the same first-order sentences.
• Completeness (Gödel, 1929): if Γ ⊨ φ then Γ ⊢ φ.

Common misconceptions

• Confusing ⊨ (truth in all models) with ⊢ (derivability) before the completeness theorem links them.
• Quantifying over subsets of the domain in a first-order formula; that is second-order logic.
• Thinking a first-order theory determines a unique structure; most theories have many non-isomorphic models.

Leads to

Optional discoveries

• Computability Church and Turing (1936) showed that no algorithm decides first-order validity, answering Hilbert's Entscheidungsproblem negatively.
• Categorical logic Categorical logic interprets first-order theories in categories other than the category of sets, such as toposes; models in sets are one special case.
• ← Set-builder notation, quantifiers and infinite sets
• ← Euclidean geometry and proof

Learning pathways

• Computer science and formal methods

Further reading

• Herbert B. Enderton, A Mathematical Introduction to Logic (1972)
• Dirk van Dalen, Logic and Structure