Basics on First-Order Semantics #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines the interpretations of first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.
Main Definitions #
first_order.language.term.realizeis defined so that
t.realize vis the term
tevaluated at variables
first_order.language.bounded_formula.realizeis defined so that
φ.realize v xsis the bounded formula
φevaluated at tuples of variables
first_order.language.formula.realizeis defined so that
φ.realize vis the formula
φevaluated at variables
first_order.language.sentence.realizeis defined so that
φ.realize Mis the sentence
φevaluated in the structure
M. Also denoted
M ⊨ φ.
first_order.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 #
first_order.language.bounded_formula.realize_to_prenexshows 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.bounded_formula α 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.bounded_formula α (n + 1), we define the formula
∀' φ : L.bounded_formula α nby universally quantifying over the variable indexed by
n : fin (n + 1).
For the Flypitch project:
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.
- f.all.realize v xs = ∀ (x : M), f.realize v (fin.snoc xs x)
- (f₁.imp f₂).realize v xs = (f₁.realize v xs → f₂.realize v xs)
- (first_order.language.bounded_formula.rel R ts).realize v xs = first_order.language.Structure.rel_map R (λ (i : fin a_5), first_order.language.term.realize (sum.elim v xs) (ts i))
- (first_order.language.bounded_formula.equal t₁ t₂).realize v xs = (first_order.language.term.realize (sum.elim v xs) t₁ = first_order.language.term.realize (sum.elim v xs) t₂)
- first_order.language.bounded_formula.falsum.realize v xs = false
A formula can be evaluated as true or false by giving values to each free variable.
The complete theory of a structure
M is the set of all sentences
Two structures are elementarily equivalent when they satisfy the same sentences.
A model of a theory is a structure in which every sentence is realized as true.
Instances of this typeclass