Basics on First-Order Semantics #
This file defines the interpretations of first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.
Main Definitions #
FirstOrder.Language.Term.realizeis defined so that
t.realize vis the term
tevaluated at variables
FirstOrder.Language.BoundedFormula.Realizeis defined so that
φ.Realize v xsis the bounded formula
φevaluated at tuples of variables
FirstOrder.Language.Formula.Realizeis defined so that
φ.Realize vis the formula
φevaluated at variables
FirstOrder.Language.Sentence.Realizeis defined so that
φ.Realize Mis the sentence
φevaluated in the structure
M. Also denoted
M ⊨ φ.
FirstOrder.Language.Theory.Modelis defined so that
T.Model Mis true if and only if every sentence of
Tis realized in
M. Also denoted
T ⊨ φ.
Main Results #
FirstOrder.Language.BoundedFormula.realize_toPrenexshows that the prenex normal form of a formula has the same realization as the original formula.
- Several results in this file show that syntactic constructions such as
subst, and the actions of language maps commute with realization of terms, formulas, sentences, and theories.
Implementation Notes #
- Formulas use a modified version of de Bruijn variables. Specifically, a
L.BoundedFormula α nis a formula with some variables indexed by a type
α, which cannot be quantified over, and some indexed by
Fin n, which can. For any
φ : L.BoundedFormula α (n + 1), we define the formula
∀' φ : L.BoundedFormula α nby universally quantifying over the variable indexed by
n : Fin (n + 1).
For the Flypitch project:
- [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
- [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
t with variables indexed by
α can be evaluated by giving a value to each variable.
A bounded formula can be evaluated as true or false by giving values to each free variable.
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.Realize FirstOrder.Language.BoundedFormula.falsum x x = False
- FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.BoundedFormula.all f) x x = ∀ (x : M), FirstOrder.Language.BoundedFormula.Realize f x (Fin.snoc x x)
A model of a theory is a structure in which every sentence is realized as true.