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] [flypitch_cpp]
- [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
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_restrictVar'
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[DecidableEq α]
{t : L.Term α}
{s : Set α}
(h : ↑t.varFinset ⊆ s)
{v : α → M}
:
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.Term.realize_varsToConstants
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
{t : L.Term (α ⊕ β)}
{v : β → M}
:
theorem
FirstOrder.Language.Term.realize_constantsVarsEquivLeft
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
{n : ℕ}
{t : (L.withConstants α).Term (β ⊕ Fin n)}
{v : β → M}
{xs : Fin n → 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)
:
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_foldr_inf
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
(l : List (L.BoundedFormula α n))
(v : α → M)
(xs : Fin n → M)
:
(List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
theorem
FirstOrder.Language.BoundedFormula.realize_foldr_imp
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{k : ℕ}
(l : List (L.BoundedFormula α k))
(f : L.BoundedFormula α k)
(v : α → M)
(xs : Fin k → M)
:
List.foldr on BoundedFormula.imp gives a big "And" of input conditions.
@[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 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_foldr_sup
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
(l : List (L.BoundedFormula α n))
(v : α → M)
(xs : Fin n → M)
:
(List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
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)
:
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)
:
theorem
FirstOrder.Language.BoundedFormula.realize_liftAt_one
{L : Language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n m : ℕ}
{φ : L.BoundedFormula α n}
{v : α → M}
{xs : Fin (n + 1) → M}
(hmn : m ≤ n)
:
@[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}
:
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)
:
@[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}
:
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}
:
@[deprecated FirstOrder.Language.Formula.realize_relabel_sumInr (since := "2025-02-21")]
theorem
FirstOrder.Language.Formula.realize_relabel_sum_inr
{L : Language}
{M : Type w}
[L.Structure M]
{n : ℕ}
(φ : L.Formula (Fin n))
{v : Empty → M}
{x : Fin n → M}
:
Alias of FirstOrder.Language.Formula.realize_relabel_sumInr.
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.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)
:
@[simp]
theorem
FirstOrder.Language.Formula.realize_equivSentence
{L : Language}
(M : Type w)
[L.Structure M]
{α : Type u'}
[(L.withConstants α).Structure M]
[(L.lhomWithConstants α).IsExpansionOn M]
(φ : L.Formula α)
:
theorem
FirstOrder.Language.Formula.realize_equivSentence_symm
{L : Language}
(M : Type w)
[L.Structure M]
{α : Type u'}
(φ : (L.withConstants α).Sentence)
(v : α → M)
:
@[simp]
theorem
FirstOrder.Language.LHom.realize_onSentence
{L : Language}
{L' : Language}
(M : Type w)
[L.Structure M]
[L'.Structure M]
(φ : L →ᴸ L')
[φ.IsExpansionOn M]
(ψ : L.Sentence)
:
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.
Equations
- L.ElementarilyEquivalent M N = (L.completeTheory M = L.completeTheory N)
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
@[simp]
theorem
FirstOrder.Language.mem_completeTheory
{L : Language}
{M : Type w}
[L.Structure M]
{φ : L.Sentence}
:
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
theorem
FirstOrder.Language.Theory.model_iff_subset_completeTheory
{L : Language}
{M : Type w}
[L.Structure M]
{T : L.Theory}
:
@[simp]
@[simp]
theorem
FirstOrder.Language.StrongHomClass.realize_boundedFormula
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
{α : Type u'}
{n : ℕ}
{F : Type u_4}
[EquivLike F M N]
[L.StrongHomClass F M N]
(g : F)
(φ : L.BoundedFormula α n)
{v : α → M}
{xs : Fin n → M}
:
theorem
FirstOrder.Language.StrongHomClass.elementarilyEquivalent
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
{F : Type u_4}
[EquivLike F M N]
[L.StrongHomClass F M N]
(g : F)
:
L.ElementarilyEquivalent M N
@[simp]
theorem
FirstOrder.Language.Relations.realize_irreflexive
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
@[simp]
theorem
FirstOrder.Language.Relations.realize_antisymmetric
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
@[simp]
theorem
FirstOrder.Language.Relations.realize_transitive
{L : Language}
{M : Type w}
[L.Structure M]
{r : L.Relations 2}
:
@[simp]
theorem
FirstOrder.Language.Sentence.realize_cardGe
(L : Language)
{M : Type w}
[L.Structure M]
(n : ℕ)
:
@[simp]
instance
FirstOrder.Language.model_infiniteTheory
(L : Language)
{M : Type w}
[L.Structure M]
[h : Infinite M]
:
@[simp]
instance
FirstOrder.Language.model_nonempty
(L : Language)
{M : Type w}
[L.Structure M]
[h : Nonempty M]
:
theorem
FirstOrder.Language.model_distinctConstantsTheory
(L : Language)
{α : Type u'}
{M : Type w}
[(L.withConstants α).Structure M]
(s : Set α)
:
theorem
FirstOrder.Language.card_le_of_model_distinctConstantsTheory
(L : Language)
{α : Type u'}
(s : Set α)
(M : Type w)
[(L.withConstants α).Structure M]
[h : M ⊨ L.distinctConstantsTheory s]
:
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
theorem
FirstOrder.Language.ElementarilyEquivalent.trans
{L : Language}
{M : Type w}
{N : Type u_1}
{P : Type u_2}
[L.Structure M]
[L.Structure N]
[L.Structure P]
(MN : L.ElementarilyEquivalent M N)
(NP : L.ElementarilyEquivalent N P)
:
L.ElementarilyEquivalent M P
theorem
FirstOrder.Language.ElementarilyEquivalent.completeTheory_eq
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
(h : L.ElementarilyEquivalent M N)
:
theorem
FirstOrder.Language.ElementarilyEquivalent.nonempty
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
[Mn : Nonempty M]
(h : L.ElementarilyEquivalent M N)
:
Nonempty N
theorem
FirstOrder.Language.ElementarilyEquivalent.infinite
{L : Language}
{M : Type w}
{N : Type u_1}
[L.Structure M]
[L.Structure N]
[Mi : Infinite M]
(h : L.ElementarilyEquivalent M N)
:
Infinite N