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 thatt.realize vis the termtevaluated at variablesv.FirstOrder.Language.BoundedFormula.Realizeis defined so thatφ.Realize v xsis the bounded formulaφevaluated at tuples of variablesvandxs.FirstOrder.Language.Formula.Realizeis defined so thatφ.Realize vis the formulaφevaluated at variablesv.FirstOrder.Language.Sentence.Realizeis defined so thatφ.Realize Mis the sentenceφevaluated in the structureM. Also denotedM ⊨ φ.FirstOrder.Language.Theory.Modelis defined so thatT.Model Mis true if and only if every sentence ofTis 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 α nis 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 α nby 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
def
FirstOrder.Language.Term.realize
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
(v : α → M)
(_t : L.Term α)
:
M
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
@[simp]
@[simp]
theorem
FirstOrder.Language.Term.realize_functions_apply₁
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{f : L.Functions 1}
{t : L.Term α}
{v : α → M}
:
realize v (f.apply₁ t) = Structure.funMap f ![realize v t]
@[simp]
theorem
FirstOrder.Language.Term.realize_functions_apply₂
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{f : L.Functions 2}
{t₁ t₂ : L.Term α}
{v : α → M}
:
realize v (f.apply₂ t₁ t₂) = Structure.funMap f ![realize v t₁, realize v t₂]
theorem
FirstOrder.Language.Term.realize_restrictVar
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[DecidableEq α]
{t : L.Term α}
{f : { x : α // x ∈ t.varFinset } → β}
{v : β → M}
(v' : α → M)
(hv' : ∀ (a : { x : α // x ∈ t.varFinset }), v (f a) = v' ↑a)
:
@[simp]
theorem
FirstOrder.Language.Term.realize_restrictVar'
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[DecidableEq α]
{t : L.Term α}
{s : Set α}
(h : ↑t.varFinset ⊆ s)
{v : α → M}
:
realize (v ∘ Subtype.val) (t.restrictVar (Set.inclusion h)) = realize v t
A special case of realize_restrictVar, included because we can add the simp attribute
to it
theorem
FirstOrder.Language.Term.realize_restrictVarLeft
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[DecidableEq α]
{γ : Type u_4}
{t : L.Term (α ⊕ γ)}
{f : { x : α // x ∈ t.varFinsetLeft } → β}
{xs : β ⊕ γ → M}
(xs' : α → M)
(hxs' : ∀ (a : { x : α // x ∈ t.varFinsetLeft }), xs (Sum.inl (f a)) = xs' ↑a)
:
@[simp]
theorem
FirstOrder.Language.Term.realize_restrictVarLeft'
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[DecidableEq α]
{γ : Type u_4}
{t : L.Term (α ⊕ γ)}
{s : Set α}
(h : ↑t.varFinsetLeft ⊆ s)
{v : α → M}
{xs : γ → M}
:
realize (Sum.elim (v ∘ Subtype.val) xs) (t.restrictVarLeft (Set.inclusion h)) = realize (Sum.elim v xs) t
A special case of realize_restrictVarLeft, included because we can add the simp attribute
to it
@[simp]
theorem
FirstOrder.Language.Term.realize_constantsToVars
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
{t : (L.withConstants α).Term β}
{v : β → M}
:
@[simp]
theorem
FirstOrder.Language.LHom.realize_onTerm
{L : Language}
{L' : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.IsExpansionOn M]
(t : L.Term α)
(v : α → M)
:
Term.realize v (φ.onTerm t) = Term.realize v t
@[simp]
theorem
FirstOrder.Language.HomClass.realize_term
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
{α : Type u'}
{F : Type u_4}
[FunLike F M N]
[L.HomClass F M N]
(g : F)
{t : L.Term α}
{v : α → M}
:
Term.realize (⇑g ∘ v) t = g (Term.realize v t)
def
FirstOrder.Language.BoundedFormula.Realize
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
(_f : L.BoundedFormula α l)
(_v : α → M)
(_xs : Fin l → M)
:
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 : M), f.Realize x✝¹ (Fin.snoc x✝ x)
Instances For
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_bdEqual
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : Fin l → M}
(t₁ t₂ : L.Term (α ⊕ Fin l))
:
(t₁.bdEqual t₂).Realize v xs ↔ Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂
@[simp]
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_rel
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : Fin l → M}
{k : ℕ}
{R : L.Relations k}
{ts : Fin k → L.Term (α ⊕ Fin l)}
:
(R.boundedFormula ts).Realize v xs ↔ Structure.RelMap R fun (i : Fin k) => Term.realize (Sum.elim v xs) (ts i)
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_rel₁
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : Fin l → M}
{R : L.Relations 1}
{t : L.Term (α ⊕ Fin l)}
:
(R.boundedFormula₁ t).Realize v xs ↔ Structure.RelMap R ![Term.realize (Sum.elim v xs) t]
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_rel₂
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : Fin l → M}
{R : L.Relations 2}
{t₁ t₂ : L.Term (α ⊕ Fin l)}
:
(R.boundedFormula₂ t₁ t₂).Realize v xs ↔ Structure.RelMap R ![Term.realize (Sum.elim v xs) t₁, Term.realize (Sum.elim v xs) t₂]
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_mapTermRel_id
{L : Language}
{L' : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[L'.Structure M]
{ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)}
{fr : (n : ℕ) → L.Relations n → L'.Relations n}
{n : ℕ}
{φ : L.BoundedFormula α n}
{v : α → M}
{v' : β → M}
{xs : Fin n → M}
(h1 :
∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M),
Term.realize (Sum.elim v' xs) (ft n t) = Term.realize (Sum.elim v xs) t)
(h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), Structure.RelMap (fr n R) x = Structure.RelMap R x)
:
(mapTermRel ft fr (fun (x : ℕ) => id) φ).Realize v' xs ↔ φ.Realize v xs
theorem
FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe
{L : Language}
{L' : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[L'.Structure M]
{k : ℕ}
{ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))}
{fr : (n : ℕ) → L.Relations n → L'.Relations n}
{n : ℕ}
{φ : L.BoundedFormula α n}
(v : {n : ℕ} → (Fin (k + n) → M) → α → M)
{v' : β → M}
(xs : Fin (k + n) → M)
(h1 :
∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
Term.realize (Sum.elim v' xs') (ft n t) = Term.realize (Sum.elim (v xs') (xs' ∘ Fin.natAdd k)) t)
(h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), Structure.RelMap (fr n R) x = Structure.RelMap R x)
(hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (Fin.snoc xs x) = v xs)
:
(mapTermRel ft fr (fun (x : ℕ) => castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ Fin.natAdd k)
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_relabel
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{m n : ℕ}
{φ : L.BoundedFormula α n}
{g : α → β ⊕ Fin m}
{v : β → M}
{xs : Fin (m + n) → M}
:
(relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m)
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_subst
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{n : ℕ}
{φ : L.BoundedFormula α n}
{tf : α → L.Term β}
{v : β → M}
{xs : Fin n → M}
:
(φ.subst tf).Realize v xs ↔ φ.Realize (fun (a : α) => Term.realize v (tf a)) xs
theorem
FirstOrder.Language.BoundedFormula.realize_restrictFreeVar
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[DecidableEq α]
{n : ℕ}
{φ : L.BoundedFormula α n}
{f : { x : α // x ∈ φ.freeVarFinset } → β}
{v : β → M}
{xs : Fin n → M}
(v' : α → M)
(hv' : ∀ (a : { x : α // x ∈ φ.freeVarFinset }), v (f a) = v' ↑a)
:
(φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
@[simp]
theorem
FirstOrder.Language.BoundedFormula.realize_restrictFreeVar'
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[DecidableEq α]
{n : ℕ}
{φ : L.BoundedFormula α n}
{s : Set α}
(h : ↑φ.freeVarFinset ⊆ s)
{v : α → M}
{xs : Fin n → M}
:
(φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ Subtype.val) xs ↔ φ.Realize v xs
A special case of realize_restrictFreeVar, included because we can add the simp attribute
to it
theorem
FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
{n : ℕ}
{φ : (L.withConstants α).BoundedFormula β n}
{v : β → M}
{xs : Fin n → M}
:
@[simp]
theorem
FirstOrder.Language.LHom.realize_onBoundedFormula
{L : Language}
{L' : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.IsExpansionOn M]
{n : ℕ}
(ψ : L.BoundedFormula α n)
{v : α → M}
{xs : Fin n → M}
:
(φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
def
FirstOrder.Language.Formula.Realize
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
(φ : L.Formula α)
(v : α → M)
:
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
@[simp]
theorem
FirstOrder.Language.Formula.realize_rel
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{k : ℕ}
{R : L.Relations k}
{ts : Fin k → L.Term α}
:
(R.formula ts).Realize v ↔ Structure.RelMap R fun (i : Fin k) => Term.realize v (ts i)
@[simp]
theorem
FirstOrder.Language.Formula.realize_rel₁
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{R : L.Relations 1}
{t : L.Term α}
:
(R.formula₁ t).Realize v ↔ Structure.RelMap R ![Term.realize v t]
@[simp]
theorem
FirstOrder.Language.Formula.realize_rel₂
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{R : L.Relations 2}
{t₁ t₂ : L.Term α}
:
(R.formula₂ t₁ t₂).Realize v ↔ Structure.RelMap R ![Term.realize v t₁, Term.realize v t₂]
@[simp]
theorem
FirstOrder.Language.Formula.realize_equal
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{t₁ t₂ : L.Term α}
{x : α → M}
:
(t₁.equal t₂).Realize x ↔ Term.realize x t₁ = Term.realize x t₂
theorem
FirstOrder.Language.Formula.boundedFormula_realize_eq_realize
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
(φ : L.Formula α)
(x : α → M)
(y : Fin 0 → M)
:
BoundedFormula.Realize φ x y ↔ φ.Realize x
def
FirstOrder.Language.Sentence.Realize
{L : Language}
(M : Type w)
[L.Structure M]
(φ : L.Sentence)
:
A sentence can be evaluated as true or false in a structure.
Equations
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
@[simp]
theorem
FirstOrder.Language.Sentence.realize_not
{L : Language}
(M : Type w)
[L.Structure M]
{φ : L.Sentence}
:
M ⊨ Formula.not φ ↔ ¬M ⊨ φ
@[simp]
theorem
FirstOrder.Language.Formula.realize_equivSentence_symm_con
{L : Language}
(M : Type w)
[L.Structure M]
{α : Type u'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
(φ : (L.withConstants α).Sentence)
:
((equivSentence.symm φ).Realize fun (a : α) => ↑(L.con a)) ↔ M ⊨ φ
theorem
FirstOrder.Language.Formula.realize_equivSentence_symm
{L : Language}
(M : Type w)
[L.Structure M]
{α : Type u'}
(φ : (L.withConstants α).Sentence)
(v : α → M)
:
(equivSentence.symm φ).Realize v ↔ M ⊨ φ
def
FirstOrder.Language.ElementarilyEquivalent
(L : Language)
(M : Type w)
(N : Type u_1)
[L.Structure M]
[L.Structure N]
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
FirstOrder.Language.model_completeTheory
{L : Language}
{M : Type w}
[L.Structure M]
:
M ⊨ L.completeTheory M
@[simp]
@[simp]
theorem
FirstOrder.Language.Relations.realize_reflexive
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.reflexive ↔ Reflexive fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Relations.realize_irreflexive
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.irreflexive ↔ Irreflexive fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Relations.realize_symmetric
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.symmetric ↔ Symmetric fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Relations.realize_antisymmetric
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.antisymmetric ↔ AntiSymmetric fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Relations.realize_transitive
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.transitive ↔ Transitive fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Relations.realize_total
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
M ⊨ r.total ↔ Total fun (x y : M) => Structure.RelMap r ![x, y]
@[simp]
theorem
FirstOrder.Language.Sentence.realize_cardGe
(L : Language)
{M : Type w}
[L.Structure M]
(n : ℕ)
:
M ⊨ Sentence.cardGe L n ↔ ↑n ≤ Cardinal.mk M
theorem
FirstOrder.Language.ElementarilyEquivalent.symm
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
(h : L.ElementarilyEquivalent M N)
:
L.ElementarilyEquivalent N M