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 that t.realize v is the term t evaluated at variables v.
• FirstOrder.Language.BoundedFormula.Realize is defined so that φ.Realize v xs is the bounded formula φ evaluated at tuples of variables v and xs.
• FirstOrder.Language.Formula.Realize is defined so that φ.Realize v is the formula φ evaluated at variables v.
• FirstOrder.Language.Sentence.Realize is defined so that φ.Realize M is the sentence φ evaluated in the structure M. Also denoted M ⊨ φ.
• FirstOrder.Language.Theory.Model is defined so that T.Model M is true if and only if every sentence of T is realized in M. Also denoted T ⊨ φ.

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 by Fin n, which can. For any φ : L.BoundedFormula α (n + 1), we define the formula ∀' φ : L.BoundedFormula α n by universally quantifying over the variable indexed by n : 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.

@[simp]

theorem FirstOrder.Language.Term.realize_var {L : Language} {M : Type w} [L.Structure M] {α : Type u'} (v : α → M) (k : α) : realize v (var k) = v k

@[simp]

theorem FirstOrder.Language.Term.realize_func {L : Language} {M : Type w} [L.Structure M] {α : Type u'} (v : α → M) {n : ℕ} (f : L.Functions n) (ts : Fin n → L.Term α) : realize v (func f ts) = Structure.funMap f fun (i : Fin n) => realize v (ts i)

@[simp]

theorem FirstOrder.Language.Term.realize_function_term {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (v : Fin n → M) (f : L.Functions n) : realize v f.term = Structure.funMap f v

@[simp]

theorem FirstOrder.Language.Term.realize_relabel {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {g : α → β} {v : β → M} : realize v (relabel g t) = realize (v ∘ g) t

@[simp]

theorem FirstOrder.Language.Term.realize_liftAt {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : ℕ} {t : L.Term (α ⊕ Fin n)} {v : α ⊕ Fin (n + n') → M} : realize v (liftAt n' m t) = realize (v ∘ Sum.map id fun (i : Fin n) => if ↑i < m then Fin.castAdd n' i else i.addNat n') t

@[simp]

theorem FirstOrder.Language.Term.realize_constants {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {c : L.Constants} {v : α → M} : realize v c.term = ↑c

@[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_con {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {A : Set M} {a : ↑A} {v : α → M} : realize v (L.con a).term = ↑a

@[simp]

theorem FirstOrder.Language.Term.realize_subst {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {tf : α → L.Term β} {v : β → M} : realize v (t.subst tf) = realize (fun (a : α) => realize v (tf a)) 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) : realize v (t.restrictVar f) = realize v' t

@[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) : realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

@[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} : realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) t.constantsToVars = realize v t

@[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} : realize v t.varsToConstants = realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) t

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} : realize (Sum.elim (Sum.elim (fun (a : α) => ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t

@[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) : Prop

A bounded formula can be evaluated as true or false by giving values to each free variable.

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M} : ⊥.Realize v xs ↔ False

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {v : α → M} {xs : Fin l → M} : φ.not.Realize v xs ↔ ¬φ.Realize v xs

@[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]

theorem FirstOrder.Language.BoundedFormula.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M} : ⊤.Realize v xs ↔ True

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_inf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l} {v : α → M} {xs : Fin l → M} : (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

@[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

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l} {v : α → M} {xs : Fin l → M} : (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.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 imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

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 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_sup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l} {v : α → M} {xs : Fin l → M} : (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

@[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

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_all {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M} : θ.all.Realize v xs ↔ ∀ (a : M), θ.Realize v (Fin.snoc xs a)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_ex {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M} : θ.ex.Realize v xs ↔ ∃ (a : M), θ.Realize v (Fin.snoc xs a)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iff {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l} {v : α → M} {xs : Fin l → M} : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

theorem FirstOrder.Language.BoundedFormula.realize_castLE_of_eq {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.BoundedFormula α m} {v : α → M} {xs : Fin n → M} : (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

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)

theorem FirstOrder.Language.BoundedFormula.realize_liftAt {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1) : (liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun (i : Fin n) => if ↑i < m then Fin.castAdd n' i else i.addNat n')

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) : (liftAt 1 m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun (i : Fin n) => if ↑i < m then i.castSucc else i.succ)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one_self {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M} : (liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.castSucc)

@[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} : (constantsVarsEquiv φ).Realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) xs ↔ φ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_relabelEquiv {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {g : α ≃ β} {k : ℕ} {φ : L.BoundedFormula α k} {v : β → M} {xs : Fin k → M} : ((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs

theorem FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self {L : Language} {M : Type w} [L.Structure M] {α : Type u'} [Nonempty M] {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin n → M} : (liftAt 1 n φ).all.Realize v xs ↔ φ.Realize v xs

@[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) : Prop

A formula can be evaluated as true or false by giving values to each free variable.

@[simp]

theorem FirstOrder.Language.Formula.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.Formula α} {v : α → M} : φ.not.Realize v ↔ ¬φ.Realize v

@[simp]

theorem FirstOrder.Language.Formula.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊥.Realize v ↔ False

@[simp]

theorem FirstOrder.Language.Formula.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊤.Realize v ↔ True

@[simp]

theorem FirstOrder.Language.Formula.realize_inf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M} : (φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formula.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M} : (φ.imp ψ).Realize v ↔ φ.Realize v → ψ.Realize v

@[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_sup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M} : (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formula.realize_iff {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M} : (φ.iff ψ).Realize v ↔ (φ.Realize v ↔ ψ.Realize v)

@[simp]

theorem FirstOrder.Language.Formula.realize_relabel {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {φ : L.Formula α} {g : α → β} {v : β → M} : (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

theorem FirstOrder.Language.Formula.realize_relabel_sumInr {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (φ : L.Formula (Fin n)) {v : Empty → M} {x : Fin n → M} : (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x

@[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} : (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x

Alias of FirstOrder.Language.Formula.realize_relabel_sumInr.

@[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₂

@[simp]

theorem FirstOrder.Language.Formula.realize_graph {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {f : L.Functions n} {x : Fin n → M} {y : M} : (graph f).Realize (Fin.cons y x) ↔ Structure.funMap f x = y

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

@[simp]

theorem FirstOrder.Language.LHom.realize_onFormula {L : Language} {L' : Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) {v : α → M} : (φ.onFormula ψ).Realize v ↔ ψ.Realize v

@[simp]

theorem FirstOrder.Language.LHom.setOf_realize_onFormula {L : Language} {L' : Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) : setOf (φ.onFormula ψ).Realize = setOf ψ.Realize

def FirstOrder.Language.Sentence.Realize {L : Language} (M : Type w) [L.Structure M] (φ : L.Sentence) : Prop

A sentence can be evaluated as true or false in a structure.

def FirstOrder.Language.«term_⊨_» : Lean.TrailingParserDescr

A sentence can be evaluated as true or false in a structure.

@[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 ⊨ φ

@[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 α) : M ⊨ equivSentence φ ↔ φ.Realize fun (a : α) => ↑(L.con a)

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 ⊨ φ

@[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) : M ⊨ φ.onSentence ψ ↔ M ⊨ ψ

def FirstOrder.Language.completeTheory (L : Language) (M : Type w) [L.Structure M] : L.Theory

The complete theory of a structure M is the set of all sentences M satisfies.

def FirstOrder.Language.ElementarilyEquivalent (L : Language) (M : Type w) (N : Type u_1) [L.Structure M] [L.Structure N] : Prop

Two structures are elementarily equivalent when they satisfy the same sentences.

def FirstOrder.«term_≅[_]_» : Lean.TrailingParserDescr

Two structures are elementarily equivalent when they satisfy the same sentences.

@[simp]

theorem FirstOrder.Language.mem_completeTheory {L : Language} {M : Type w} [L.Structure M] {φ : L.Sentence} : φ ∈ L.completeTheory M ↔ M ⊨ φ

theorem FirstOrder.Language.elementarilyEquivalent_iff {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] : L.ElementarilyEquivalent M N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ

class FirstOrder.Language.Theory.Model {L : Language} (M : Type w) [L.Structure M] (T : L.Theory) : Prop

A model of a theory is a structure in which every sentence is realized as true.

• realize_of_mem (φ : L.Sentence) : φ ∈ T → M ⊨ φ

def FirstOrder.Language.«term_⊨__1» : Lean.TrailingParserDescr

A model of a theory is a structure in which every sentence is realized as true.

@[simp]

theorem FirstOrder.Language.Theory.model_iff {L : Language} {M : Type w} [L.Structure M] (T : L.Theory) : M ⊨ T ↔ ∀ φ ∈ T, M ⊨ φ

theorem FirstOrder.Language.Theory.realize_sentence_of_mem {L : Language} {M : Type w} [L.Structure M] (T : L.Theory) [M ⊨ T] {φ : L.Sentence} (h : φ ∈ T) : M ⊨ φ

@[simp]

theorem FirstOrder.Language.LHom.onTheory_model {L : Language} {L' : Language} {M : Type w} [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) : M ⊨ φ.onTheory T ↔ M ⊨ T

instance FirstOrder.Language.model_empty {L : Language} {M : Type w} [L.Structure M] : M ⊨ ∅

theorem FirstOrder.Language.Theory.Model.mono {L : Language} {M : Type w} [L.Structure M] {T T' : L.Theory} (_h : M ⊨ T') (hs : T ⊆ T') : M ⊨ T

theorem FirstOrder.Language.Theory.Model.union {L : Language} {M : Type w} [L.Structure M] {T T' : L.Theory} (h : M ⊨ T) (h' : M ⊨ T') : M ⊨ T ∪ T'

@[simp]

theorem FirstOrder.Language.Theory.model_union_iff {L : Language} {M : Type w} [L.Structure M] {T T' : L.Theory} : M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T'

@[simp]

theorem FirstOrder.Language.Theory.model_singleton_iff {L : Language} {M : Type w} [L.Structure M] {φ : L.Sentence} : M ⊨ {φ} ↔ M ⊨ φ

theorem FirstOrder.Language.Theory.model_insert_iff {L : Language} {M : Type w} [L.Structure M] {T : L.Theory} {φ : L.Sentence} : M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T

theorem FirstOrder.Language.Theory.model_iff_subset_completeTheory {L : Language} {M : Type w} [L.Structure M] {T : L.Theory} : M ⊨ T ↔ T ⊆ L.completeTheory M

theorem FirstOrder.Language.Theory.completeTheory.subset {L : Language} {M : Type w} [L.Structure M] {T : L.Theory} [MT : M ⊨ T] : T ⊆ L.completeTheory M

instance FirstOrder.Language.model_completeTheory {L : Language} {M : Type w} [L.Structure M] : M ⊨ L.completeTheory M

theorem FirstOrder.Language.realize_iff_of_model_completeTheory {L : Language} (M : Type w) (N : Type u_1) [L.Structure M] [L.Structure N] [N ⊨ L.completeTheory M] (φ : L.Sentence) : N ⊨ φ ↔ M ⊨ φ

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_alls {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} : φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_exs {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} : φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs

@[simp]

theorem FirstOrder.Language.Formula.realize_iAlls {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} : (iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun (a : α ⊕ β) => Sum.elim v i a

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iAlls {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} {v' : Fin 0 → M} : Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize fun (a : α ⊕ β) => Sum.elim v i a

@[simp]

theorem FirstOrder.Language.Formula.realize_iExs {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {γ : Type u_3} [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} : (iExs γ φ).Realize v ↔ ∃ (i : γ → M), φ.Realize (Sum.elim v i)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iExs {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {γ : Type u_3} [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M} : Realize (Formula.iExs γ φ) v v' ↔ ∃ (i : γ → M), φ.Realize (Sum.elim v i)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_toFormula {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) (v : α ⊕ Fin n → M) : φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} [Finite β] {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M} : (iSup f).Realize v v' ↔ ∃ (b : β), (f b).Realize v v'

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iInf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} [Finite β] {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M} : (iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'

@[simp]

theorem FirstOrder.Language.Formula.realize_iSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [Finite β] {f : β → L.Formula α} {v : α → M} : (iSup f).Realize v ↔ ∃ (b : β), (f b).Realize v

@[simp]

theorem FirstOrder.Language.Formula.realize_iInf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [Finite β] {f : β → L.Formula α} {v : α → M} : (iInf f).Realize v ↔ ∀ (b : β), (f b).Realize v

theorem FirstOrder.Language.Formula.realize_iExsUnique {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {γ : Type u_3} [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} : (iExsUnique γ φ).Realize v ↔ ∃! i : γ → M, φ.Realize (Sum.elim v i)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_iExsUnique {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {γ : Type u_3} [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M} : Realize (Formula.iExsUnique γ φ) v v' ↔ ∃! i : γ → M, φ.Realize (Sum.elim v i)

@[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} : φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs

@[simp]

theorem FirstOrder.Language.StrongHomClass.realize_formula {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.Formula α) {v : α → M} : φ.Realize (⇑g ∘ v) ↔ φ.Realize v

theorem FirstOrder.Language.StrongHomClass.realize_sentence {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.Sentence) : M ⊨ φ ↔ N ⊨ φ

theorem FirstOrder.Language.StrongHomClass.theory_model {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) [M ⊨ T] : N ⊨ T

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_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

@[simp]

theorem FirstOrder.Language.model_infiniteTheory_iff (L : Language) {M : Type w} [L.Structure M] : M ⊨ L.infiniteTheory ↔ Infinite M

instance FirstOrder.Language.model_infiniteTheory (L : Language) {M : Type w} [L.Structure M] [h : Infinite M] : M ⊨ L.infiniteTheory

@[simp]

theorem FirstOrder.Language.model_nonemptyTheory_iff (L : Language) {M : Type w} [L.Structure M] : M ⊨ L.nonemptyTheory ↔ Nonempty M

instance FirstOrder.Language.model_nonempty (L : Language) {M : Type w} [L.Structure M] [h : Nonempty M] : M ⊨ L.nonemptyTheory

theorem FirstOrder.Language.model_distinctConstantsTheory (L : Language) {α : Type u'} {M : Type w} [(L.withConstants α).Structure M] (s : Set α) : M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun (i : α) => ↑(L.con i)) s

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] : Cardinal.lift.{w, u'} (Cardinal.mk ↑s) ≤ Cardinal.lift.{u', w} (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

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) : L.completeTheory M = L.completeTheory N

theorem FirstOrder.Language.ElementarilyEquivalent.realize_sentence {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) (φ : L.Sentence) : M ⊨ φ ↔ N ⊨ φ

theorem FirstOrder.Language.ElementarilyEquivalent.theory_model_iff {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} (h : L.ElementarilyEquivalent M N) : M ⊨ T ↔ N ⊨ T

theorem FirstOrder.Language.ElementarilyEquivalent.theory_model {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} [MT : M ⊨ T] (h : L.ElementarilyEquivalent M N) : N ⊨ T

theorem FirstOrder.Language.ElementarilyEquivalent.nonempty_iff {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) : Nonempty M ↔ Nonempty 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_iff {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) : Infinite M ↔ Infinite 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