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.realize
is defined so thatt.realize v
is the termt
evaluated at variablesv
.FirstOrder.Language.BoundedFormula.Realize
is defined so thatφ.Realize v xs
is the bounded formulaφ
evaluated at tuples of variablesv
andxs
.FirstOrder.Language.Formula.Realize
is defined so thatφ.Realize v
is the formulaφ
evaluated at variablesv
.FirstOrder.Language.Sentence.Realize
is defined so thatφ.Realize M
is the sentenceφ
evaluated in the structureM
. Also denotedM ⊨ φ
.FirstOrder.Language.Theory.Model
is defined so thatT.Model M
is true if and only if every sentence ofT
is realized inM
. Also denotedT ⊨ φ
.
Main Results #
- Several results in this file show that syntactic constructions such as
relabel
,castLE
,liftAt
,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 α n
is a formula with some variables indexed by a typeα
, which cannot be quantified over, and some indexed byFin n
, which can. For anyφ : L.BoundedFormula α (n + 1)
, we define the formula∀' φ : L.BoundedFormula α n
by universally quantifying over the variable indexed byn : Fin (n + 1)
.
References #
For the Flypitch project:
- [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [HvD20]
- J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
A term t
with variables indexed by α
can be evaluated by giving a value to each variable.
Equations
- FirstOrder.Language.Term.realize v (FirstOrder.Language.var k) = v k
- FirstOrder.Language.Term.realize v (FirstOrder.Language.func f ts) = FirstOrder.Language.Structure.funMap f fun (i : Fin l) => FirstOrder.Language.Term.realize v (ts i)
Instances For
A bounded formula can be evaluated as true or false by giving values to each free variable.
Equations
- FirstOrder.Language.BoundedFormula.falsum.Realize x✝ x = False
- (FirstOrder.Language.BoundedFormula.equal t₁ t₂).Realize x✝ x = (FirstOrder.Language.Term.realize (Sum.elim x✝ x) t₁ = FirstOrder.Language.Term.realize (Sum.elim x✝ x) t₂)
- (FirstOrder.Language.BoundedFormula.rel R ts).Realize x✝ x = FirstOrder.Language.Structure.RelMap R fun (i : Fin l) => FirstOrder.Language.Term.realize (Sum.elim x✝ x) (ts i)
- (f₁.imp f₂).Realize x✝ x = (f₁.Realize x✝ x → f₂.Realize x✝ x)
- f.all.Realize x✝ x = ∀ (x_1 : M), f.Realize x✝ (Fin.snoc x x_1)
Instances For
A formula can be evaluated as true or false by giving values to each free variable.
Equations
- φ.Realize v = FirstOrder.Language.BoundedFormula.Realize φ v default
Instances For
A sentence can be evaluated as true or false in a structure.
Equations
- M ⊨ φ = FirstOrder.Language.Formula.Realize φ default
Instances For
A sentence can be evaluated as true or false in a structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complete theory of a structure M
is the set of all sentences M
satisfies.
Instances For
Two structures are elementarily equivalent when they satisfy the same sentences.
Instances For
Two structures are elementarily equivalent when they satisfy the same sentences.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A model of a theory is a structure in which every sentence is realized as true.
- realize_of_mem : ∀ φ ∈ T, M ⊨ φ
Instances
A model of a theory is a structure in which every sentence is realized as true.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯