Primeros años de universidadFoundationsPlanificado
First-order logic
The formal language of quantifiers: signatures, terms and formulas, structures and satisfaction, and a deductive system, with soundness proved and completeness stated.
math.found.first-order-logic
La lección de este tema todavía no se ha escrito. El esquema siguiente forma parte del mapa del plan de estudios y no ha sido revisado.
Se basa en
Requisitos previos obligatorios, hasta el fondo: 5
Aprenderás a
- 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.
Definición
- 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.
Teorema
- Soundness: if Γ ⊢ φ then Γ ⊨ φ.
- Isomorphic structures satisfy exactly the same first-order sentences.
- Completeness (Gödel, 1929): if Γ ⊨ φ then Γ ⊢ φ.
Errores frecuentes
- 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.
Conduce a
Descubrimientos opcionales
- 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
Itinerarios de aprendizaje
Lecturas complementarias
- Herbert B. Enderton, A Mathematical Introduction to Logic (1972)
- Dirk van Dalen, Logic and Structure