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

• FirstOrder.Language.BoundedFormula.realize_toPrenex shows 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 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 : FirstOrder.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)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Term.realize_liftAt {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {n' : ℕ} {m : ℕ} {t : L.Term (α ⊕ Fin n)} {v : α ⊕ Fin (n + n') → M} : FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.liftAt n' m t) = FirstOrder.Language.Term.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {c : L.Constants} {v : α → M} : FirstOrder.Language.Term.realize v c.term = ↑c

@[simp]

theorem FirstOrder.Language.Term.realize_functions_apply₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.Functions 1} {t : L.Term α} {v : α → M} : FirstOrder.Language.Term.realize v (f.apply₁ t) = FirstOrder.Language.Structure.funMap f ![FirstOrder.Language.Term.realize v t]

@[simp]

theorem FirstOrder.Language.Term.realize_functions_apply₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.Functions 2} {t₁ : L.Term α} {t₂ : L.Term α} {v : α → M} : FirstOrder.Language.Term.realize v (f.apply₂ t₁ t₂) = FirstOrder.Language.Structure.funMap f ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]

theorem FirstOrder.Language.Term.realize_con {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {A : Set M} {a : ↑A} {v : α → M} : FirstOrder.Language.Term.realize v (L.con a).term = ↑a

@[simp]

theorem FirstOrder.Language.Term.realize_subst {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {tf : α → L.Term β} {v : β → M} : FirstOrder.Language.Term.realize v (t.subst tf) = FirstOrder.Language.Term.realize (fun (a : α) => FirstOrder.Language.Term.realize v (tf a)) t

@[simp]

theorem FirstOrder.Language.Term.realize_restrictVar {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [DecidableEq α] {t : L.Term α} {s : Set α} (h : ↑t.varFinset ⊆ s) {v : α → M} : FirstOrder.Language.Term.realize (v ∘ Subtype.val) (t.restrictVar (Set.inclusion h)) = FirstOrder.Language.Term.realize v t

@[simp]

theorem FirstOrder.Language.Term.realize_restrictVarLeft {L : FirstOrder.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} : FirstOrder.Language.Term.realize (Sum.elim (v ∘ Subtype.val) xs) (t.restrictVarLeft (Set.inclusion h)) = FirstOrder.Language.Term.realize (Sum.elim v xs) t

@[simp]

theorem FirstOrder.Language.Term.realize_constantsToVars {L : FirstOrder.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} : FirstOrder.Language.Term.realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) t.constantsToVars = FirstOrder.Language.Term.realize v t

@[simp]

theorem FirstOrder.Language.Term.realize_varsToConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {t : L.Term (α ⊕ β)} {v : β → M} : FirstOrder.Language.Term.realize v t.varsToConstants = FirstOrder.Language.Term.realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) t

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

@[simp]

theorem FirstOrder.Language.LHom.realize_onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (t : L.Term α) (v : α → M) : FirstOrder.Language.Term.realize v (φ.onTerm t) = FirstOrder.Language.Term.realize v t

@[simp]

theorem FirstOrder.Language.Hom.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} (g : L.Hom M N) {t : L.Term α} {v : α → M} : FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)

@[simp]

theorem FirstOrder.Language.Embedding.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {v : α → M} (t : L.Term α) (g : L.Embedding M N) : FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)

@[simp]

theorem FirstOrder.Language.Equiv.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {v : α → M} (t : L.Term α) (g : L.Equiv M N) : FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)

def FirstOrder.Language.BoundedFormula.Realize {L : FirstOrder.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.

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)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_bot {L : FirstOrder.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 : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M} (t₁ : L.Term (α ⊕ Fin l)) (t₂ : L.Term (α ⊕ Fin l)) : (t₁.bdEqual t₂).Realize v xs ↔ FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ = FirstOrder.Language.Term.realize (Sum.elim v xs) t₂

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_top {L : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α 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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) : (List.foldr (fun (x x_1 : L.BoundedFormula α n) => x ⊓ x_1) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_rel {L : FirstOrder.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 ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_rel₁ {L : FirstOrder.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 ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t]

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M} {R : L.Relations 2} {t₁ : L.Term (α ⊕ Fin l)} {t₂ : L.Term (α ⊕ Fin l)} : (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t₁, FirstOrder.Language.Term.realize (Sum.elim v xs) t₂]

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α 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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) : (List.foldr (fun (x x_1 : L.BoundedFormula α n) => x ⊔ x_1) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_all {L : FirstOrder.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 : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α 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 : FirstOrder.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} : (FirstOrder.Language.BoundedFormula.castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_id {L : FirstOrder.Language} {L' : FirstOrder.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), FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t) (h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) : (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun (x : ℕ) => id) φ).Realize v' xs ↔ φ.Realize v xs

theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe {L : FirstOrder.Language} {L' : FirstOrder.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), FirstOrder.Language.Term.realize (Sum.elim v' xs') (ft n t) = FirstOrder.Language.Term.realize (Sum.elim (v xs') (xs' ∘ Fin.natAdd k)) t) (h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) (hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (Fin.snoc xs x) = v xs) : (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun (n : ℕ) => FirstOrder.Language.BoundedFormula.castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ Fin.natAdd k)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_relabel {L : FirstOrder.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} : (FirstOrder.Language.BoundedFormula.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 : FirstOrder.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) : (FirstOrder.Language.BoundedFormula.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M} (hmn : m ≤ n) : (FirstOrder.Language.BoundedFormula.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M} : (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.castSucc)

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_subst {L : FirstOrder.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 : α) => FirstOrder.Language.Term.realize v (tf a)) xs

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar {L : FirstOrder.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

theorem FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv {L : FirstOrder.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} : (FirstOrder.Language.BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun (a : α) => ↑(L.con a)) v) xs ↔ φ.Realize v xs

@[simp]

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

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

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsPrenex) {v : α → M} {xs : Fin n → M} : (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsPrenex) (hψ : ψ.IsPrenex) {v : α → M} {xs : Fin n → M} : (φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

@[simp]

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

@[simp]

theorem FirstOrder.Language.LHom.realize_onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.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 : FirstOrder.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.

Equations

• φ.Realize v = FirstOrder.Language.BoundedFormula.Realize φ v default

@[simp]

theorem FirstOrder.Language.Formula.realize_not {L : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊥.Realize v ↔ False

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Formula.realize_rel {L : FirstOrder.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 ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => FirstOrder.Language.Term.realize v (ts i)

@[simp]

theorem FirstOrder.Language.Formula.realize_rel₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {R : L.Relations 1} {t : L.Term α} : (R.formula₁ t).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t]

@[simp]

theorem FirstOrder.Language.Formula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {R : L.Relations 2} {t₁ : L.Term α} {t₂ : L.Term α} : (R.formula₂ t₁ t₂).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem FirstOrder.Language.Formula.realize_equal {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {t₁ : L.Term α} {t₂ : L.Term α} {x : α → M} : (t₁.equal t₂).Realize x ↔ FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂

@[simp]

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

@[simp]

theorem FirstOrder.Language.LHom.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.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 : FirstOrder.Language} {L' : FirstOrder.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 : FirstOrder.Language} (M : Type w) [L.Structure M] (φ : L.Sentence) : Prop

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

Equations

• M ⊨ φ = FirstOrder.Language.Formula.Realize φ default

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

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.

@[simp]

theorem FirstOrder.Language.Sentence.realize_not {L : FirstOrder.Language} (M : Type w) [L.Structure M] {φ : L.Sentence} : M ⊨ FirstOrder.Language.Formula.not φ ↔ ¬M ⊨ φ

@[simp]

theorem FirstOrder.Language.Formula.realize_equivSentence_symm_con {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] (φ : (L.withConstants α).Sentence) : ((FirstOrder.Language.Formula.equivSentence.symm φ).Realize fun (a : α) => ↑(L.con a)) ↔ M ⊨ φ

@[simp]

theorem FirstOrder.Language.Formula.realize_equivSentence {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] (φ : L.Formula α) : M ⊨ FirstOrder.Language.Formula.equivSentence φ ↔ φ.Realize fun (a : α) => ↑(L.con a)

theorem FirstOrder.Language.Formula.realize_equivSentence_symm {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} (φ : (L.withConstants α).Sentence) (v : α → M) : (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v ↔ M ⊨ φ

@[simp]

theorem FirstOrder.Language.LHom.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type w) [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Sentence) : M ⊨ φ.onSentence ψ ↔ M ⊨ ψ

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

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

Equations

• L.completeTheory M = {φ : L.Sentence | M ⊨ φ}

def FirstOrder.Language.ElementarilyEquivalent (L : FirstOrder.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.

Equations

• L.ElementarilyEquivalent M N = (L.completeTheory M = L.completeTheory N)

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem FirstOrder.Language.elementarilyEquivalent_iff {L : FirstOrder.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 : FirstOrder.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 : ∀ φ ∈ T, M ⊨ φ

theorem FirstOrder.Language.Theory.Model.realize_of_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} [self : M ⊨ T] (φ : 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem FirstOrder.Language.Theory.realize_sentence_of_mem {L : FirstOrder.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 : FirstOrder.Language} {L' : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] : M ⊨ ∅

Equations

• ⋯ = ⋯

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

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

@[simp]

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

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

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

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

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

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.realize_iff_of_model_completeTheory {L : FirstOrder.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 : FirstOrder.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 : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {γ : Type u_3} [Finite γ] {f : α → β ⊕ γ} {φ : L.Formula α} {v : β → M} : (FirstOrder.Language.Formula.iAlls f φ).Realize v ↔ ∀ (i : γ → M), φ.Realize fun (a : α) => Sum.elim v i (f a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_toFormula {L : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} (s : Finset β) (f : β → L.BoundedFormula α n) (v : α → M) (v' : Fin n → M) : (FirstOrder.Language.BoundedFormula.iSup s f).Realize v v' ↔ ∃ b ∈ s, (f b).Realize v v'

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.realize_boundedFormula {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {n : ℕ} (g : L.Equiv M N) (φ : L.BoundedFormula α n) {v : α → M} {xs : Fin n → M} : φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs

@[simp]

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

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

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

theorem FirstOrder.Language.Equiv.elementarilyEquivalent {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (g : L.Equiv M N) : L.ElementarilyEquivalent M N

@[simp]

theorem FirstOrder.Language.Relations.realize_reflexive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.reflexive ↔ Reflexive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Relations.realize_irreflexive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.irreflexive ↔ Irreflexive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Relations.realize_symmetric {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.symmetric ↔ Symmetric fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Relations.realize_antisymmetric {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.antisymmetric ↔ AntiSymmetric fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Relations.realize_transitive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.transitive ↔ Transitive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Relations.realize_total {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} : M ⊨ r.total ↔ Total fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem FirstOrder.Language.Sentence.realize_cardGe (L : FirstOrder.Language) {M : Type w} [L.Structure M] (n : ℕ) : M ⊨ FirstOrder.Language.Sentence.cardGe L n ↔ ↑n ≤ Cardinal.mk M

@[simp]

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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