Semantics of first-order logic

This file defines the semantics of first-order logic (structures, models, satisfiability, etc.).

class FirstOrder.Language.HasStructure (L : Language) (M : Type u) : Type u

First-order structures.

• interpFunc {m : ℕ} : L.Func m → Vec M m → M
• interpRel {m : ℕ} : L.Rel m → Vec M m → Prop

def FirstOrder.Language.interp {L : Language} {n : ℕ} (M : Type u) [L.HasStructure M] : L.Term n → Vec M n → M

A term is interpreted by a structures and an assignment of type Vec M n.

Equations

• ⟦#x_2⟧ₜ M, x✝ = x✝ x_2
• ⟦f ⬝ᶠ v⟧ₜ M, x✝ = FirstOrder.Language.HasStructure.interpFunc f fun (i : Fin m) => ⟦v i⟧ₜ M, x✝

def FirstOrder.Language.«term⟦_⟧ₜ_,_» : Lean.ParserDescr

Equations

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

@[simp]

theorem FirstOrder.Language.interp_var {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {ρ : Vec M n} {i : Fin n} : ⟦#i⟧ₜ M, ρ = ρ i

@[simp]

theorem FirstOrder.Language.interp_func {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {f : L.Func m} {v : Vec (L.Term n) m} : ⟦f ⬝ᶠ v⟧ₜ M, ρ = HasStructure.interpFunc f fun (i : Fin m) => ⟦v i⟧ₜ M, ρ

theorem FirstOrder.Language.interp_subst {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {t : L.Term n} {σ : L.Subst n m} {ρ : Vec M m} : ⟦t[σ]ₜ⟧ₜ M, ρ = ⟦t⟧ₜ M, fun (x : Fin n) => ⟦σ x⟧ₜ M, ρ

theorem FirstOrder.Language.interp_shift_succ {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {t : L.Term n} {k : ℕ} {u : M} {ρ : Vec M (n + k)} : ⟦↑ₜ^[k + 1] t⟧ₜ M, u ∷ᵥ ρ = ⟦↑ₜ^[k] t⟧ₜ M, ρ

theorem FirstOrder.Language.interp_shift {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {t : L.Term n} {ρ : Vec M n} {u : M} : ⟦↑ₜt⟧ₜ M, u ∷ᵥ ρ = ⟦t⟧ₜ M, ρ

def FirstOrder.Language.satisfy {L : Language} (M : Type u) [L.HasStructure M] {n : ℕ} : L.Formula n → Vec M n → Prop

A formula is satisfied by a structure and an assignment if it is interpreted as true.

Equations

• (M ⊨[x✝] r ⬝ʳ v) = FirstOrder.Language.HasStructure.interpRel r fun (i : Fin m) => ⟦v i⟧ₜ M, x✝
• (M ⊨[x✝] t₁ ≐ t₂) = (⟦t₁⟧ₜ M, x✝ = ⟦t₂⟧ₜ M, x✝)
• (M ⊨[x✝] FirstOrder.Language.Formula.false) = False
• (M ⊨[x✝] p.imp q) = (M ⊨[x✝] p → M ⊨[x✝] q)
• (M ⊨[x✝] ∀' p) = ∀ (u : M), M ⊨[u ∷ᵥ x✝] p

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

Equations

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

@[simp]

theorem FirstOrder.Language.satisfy_rel {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {r : L.Rel m} {v : Vec (L.Term n) m} : M ⊨[ρ] r ⬝ʳ v ↔ HasStructure.interpRel r fun (i : Fin m) => ⟦v i⟧ₜ M, ρ

@[simp]

theorem FirstOrder.Language.satisfy_eq {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {t₁ t₂ : L.Term n} {ρ : Vec M n} : M ⊨[ρ] t₁ ≐ t₂ ↔ ⟦t₁⟧ₜ M, ρ = ⟦t₂⟧ₜ M, ρ

@[simp]

theorem FirstOrder.Language.satisfy_false {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {ρ : Vec M n} : ¬M ⊨[ρ] ⊥

@[simp]

theorem FirstOrder.Language.satisfy_imp {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p q : L.Formula n} {ρ : Vec M n} : M ⊨[ρ] p ⇒ q ↔ M ⊨[ρ] p → M ⊨[ρ] q

@[simp]

theorem FirstOrder.Language.satisfy_true {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {ρ : Vec M n} : M ⊨[ρ] ⊤

@[simp]

theorem FirstOrder.Language.satisfy_neg {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p : L.Formula n} {ρ : Vec M n} : M ⊨[ρ] ~ p ↔ ¬M ⊨[ρ] p

@[simp]

theorem FirstOrder.Language.satisfy_and {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p q : L.Formula n} {ρ : Vec M n} : M ⊨[ρ] p ⩑ q ↔ M ⊨[ρ] p ∧ M ⊨[ρ] q

@[simp]

theorem FirstOrder.Language.satisfy_or {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p q : L.Formula n} {ρ : Vec M n} : M ⊨[ρ] p ⩒ q ↔ M ⊨[ρ] p ∨ M ⊨[ρ] q

@[simp]

theorem FirstOrder.Language.satisfy_iff {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p q : L.Formula n} {ρ : Vec M n} : M ⊨[ρ] p ⇔ q ↔ (M ⊨[ρ] p ↔ M ⊨[ρ] q)

@[simp]

theorem FirstOrder.Language.satisfy_all {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {ρ : Vec M n} {p : L.Formula (n + 1)} : M ⊨[ρ] ∀' p ↔ ∀ (u : M), M ⊨[u ∷ᵥ ρ] p

@[simp]

theorem FirstOrder.Language.satisfy_ex {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {ρ : Vec M n} {p : L.Formula (n + 1)} : M ⊨[ρ] ∃' p ↔ ∃ (u : M), M ⊨[u ∷ᵥ ρ] p

@[simp]

theorem FirstOrder.Language.satisfy_vecAnd {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {v : Vec (L.Formula n) m} : M ⊨[ρ] ⋀ (i : Fin m), v i ↔ ∀ (i : Fin m), M ⊨[ρ] v i

@[simp]

theorem FirstOrder.Language.satisfy_vecOr {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {v : Vec (L.Formula n) m} : M ⊨[ρ] ⋁ (i : Fin m), v i ↔ ∃ (i : Fin m), M ⊨[ρ] v i

@[simp]

theorem FirstOrder.Language.satisfy_allN {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {p : L.Formula (n + m)} : M ⊨[ρ] ∀^[m] p ↔ ∀ (v : Vec M m), M ⊨[v ++ᵥ ρ] p

@[simp]

theorem FirstOrder.Language.satisfy_exN {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {ρ : Vec M n} {p : L.Formula (n + m)} : M ⊨[ρ] ∃^[m] p ↔ ∃ (v : Vec M m), M ⊨[v ++ᵥ ρ] p

theorem FirstOrder.Language.satisfy_subst {L : Language} {M : Type u} [L.HasStructure M] {m n : ℕ} {p : L.Formula n} {σ : L.Subst n m} {ρ : Vec M m} : M ⊨[ρ] p[σ]ₚ ↔ M ⊨[fun (x : Fin n) => ⟦σ x⟧ₜ M, ρ] p

theorem FirstOrder.Language.satisfy_subst_single {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {t : L.Term n} {ρ : Vec M n} {p : L.Formula (n + 1)} : M ⊨[ρ] p[↦ₛ t]ₚ ↔ M ⊨[(⟦t⟧ₜ M, ρ) ∷ᵥ ρ] p

theorem FirstOrder.Language.satisfy_subst_assign {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p : L.Formula (n + 1)} {t : L.Term (n + 1)} {ρ : Vec M (n + 1)} : M ⊨[ρ] p[≔ₛ t]ₚ ↔ M ⊨[(⟦t⟧ₜ M, ρ) ∷ᵥ ρ.tail] p

theorem FirstOrder.Language.satisfy_shift_succ {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p : L.Formula n} {k : ℕ} {u : M} {ρ : Vec M (n + k)} : M ⊨[u ∷ᵥ ρ] ↑ₚ^[k + 1] p ↔ M ⊨[ρ] ↑ₚ^[k] p

theorem FirstOrder.Language.satisfy_shift {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p : L.Formula n} {ρ : Vec M n} {u : M} : M ⊨[u ∷ᵥ ρ] ↑ₚp ↔ M ⊨[ρ] p

@[reducible, inline]

abbrev FirstOrder.Language.satisfys {L : Language} (M : Type u) [L.HasStructure M] (p : L.Sentence) : Prop

Equations

• (M ⊨ₛ p) = (M ⊨[[]ᵥ] p)

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

Equations

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

theorem FirstOrder.Language.satisfy_alls {L : Language} {M : Type u} [L.HasStructure M] {n : ℕ} {p : L.Formula n} : M ⊨ₛ ∀* p ↔ ∀ (ρ : Vec M n), M ⊨[ρ] p

structure FirstOrder.Language.Structure (L : Language) : Type (u + 1)

Bundled version of HasStructure.

• Dom : Type u
• interpFunc {m : ℕ} : L.Func m → Vec self.Dom m → self.Dom
• interpRel {m : ℕ} : L.Rel m → Vec self.Dom m → Prop

instance FirstOrder.Language.Structure.instCoeSortType {L : Language} : CoeSort L.Structure (Type u)

Equations

• FirstOrder.Language.Structure.instCoeSortType = { coe := fun (x : L.Structure) => x.Dom }

instance FirstOrder.Language.Structure.instHasStructureDom {L : Language} {M : L.Structure} : L.HasStructure M.Dom

Equations

• FirstOrder.Language.Structure.instHasStructureDom = { interpFunc := fun {m : ℕ} => M.interpFunc, interpRel := fun {m : ℕ} => M.interpRel }

@[reducible, inline]

abbrev FirstOrder.Language.Structure.of {L : Language} (M : Type u) [L.HasStructure M] : L.Structure

Equations

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

def FirstOrder.Language.Entails {L : Language} {n : ℕ} (Γ : L.FormulaSet n) (p : L.Formula n) : Prop

Γ ⊨ p (Γ entails p) if any structure that satisfies Γ must also satisfy p.

Equations

• (Γ ⊨ p) = ∀ (M : L.Structure) (ρ : Vec M.Dom n), (∀ q ∈ Γ, M.Dom ⊨[ρ] q) → M.Dom ⊨[ρ] p

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

Equations

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

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

Equations

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

def FirstOrder.Language.Satisfiable {L : Language} {n : ℕ} (Γ : L.FormulaSet n) : Prop

Γ is satisfiable if there is a structure and an assignment that satisfy all formulas in Γ. The assignment is not needed for Theory (see Theory.satisfiable_iff).

Equations

• FirstOrder.Language.Satisfiable.{?u.21} Γ = ∃ (M : L.Structure) (ρ : Vec M.Dom n), ∀ p ∈ Γ, M.Dom ⊨[ρ] p

theorem FirstOrder.Language.Satisfiable.weaken {L : Language} {n : ℕ} {Γ Δ : L.FormulaSet n} : Γ ⊆ Δ → Satisfiable.{u} Δ → Satisfiable.{u} Γ

theorem FirstOrder.Language.Satisfiable.empty {L : Language} {n : ℕ} : Satisfiable.{u_1} ∅

class FirstOrder.Language.Theory.IsModel {L : Language} (T : L.Theory) (M : Type u) [L.HasStructure M] : Prop

A structure M is a model of theory T if it satisfies all the axioms of T.

• satisfy_theory (p : L.Sentence) : p ∈ T → M ⊨ₛ p

structure FirstOrder.Language.Theory.Model {L : Language} (T : L.Theory) extends L.Structure : Type (u_1 + 1)

Bundled version of IsModel.

• Dom : Type u_1
• interpFunc {m : ℕ} : L.Func m → Vec self.Dom m → self.Dom
• interpRel {m : ℕ} : L.Rel m → Vec self.Dom m → Prop
• satisfy_theory (p : L.Sentence) : p ∈ T → self.Dom ⊨ₛ p

instance FirstOrder.Language.Theory.Model.instCoeOutStructure {L : Language} {T : L.Theory} : CoeOut T.Model L.Structure

Equations

• FirstOrder.Language.Theory.Model.instCoeOutStructure = { coe := fun (x : T.Model) => x.toStructure }

instance FirstOrder.Language.Theory.Model.instCoeSortType {L : Language} {T : L.Theory} : CoeSort T.Model (Type u)

Equations

• FirstOrder.Language.Theory.Model.instCoeSortType = { coe := fun (x : T.Model) => x.Dom }

instance FirstOrder.Language.Theory.Model.instIsModelDom {L : Language} {T : L.Theory} {M : T.Model} : T.IsModel M.Dom

@[reducible, inline]

abbrev FirstOrder.Language.Theory.Model.of {L : Language} {T : L.Theory} (M : Type u) [L.HasStructure M] [T.IsModel M] : T.Model

Equations

• FirstOrder.Language.Theory.Model.of M = { toStructure := FirstOrder.Language.Structure.of M, satisfy_theory := ⋯ }

theorem FirstOrder.Language.Theory.entails_iff {L : Language} {T : L.Theory} {p : L.Sentence} : T ⊨ p ↔ ∀ (M : T.Model), M.Dom ⊨ₛ p

theorem FirstOrder.Language.Theory.satisfiable_iff {L : Language} {T : L.Theory} : Satisfiable.{u} T ↔ Nonempty T.Model

def FirstOrder.Language.Satisfiable.of_model {L : Language} {T : L.Theory} (M : Type u) [L.HasStructure M] [T.IsModel M] : Satisfiable.{u} T

Equations

• ⋯ = ⋯

def FirstOrder.Language.theory (L : Language) (M : Type u) [L.HasStructure M] : L.Theory

The theory of a structure M includes all the sentences satisfied by M as its axioms.

Equations

• L.theory M = {p : L.Sentence | M ⊨ₛ p}

instance FirstOrder.Language.instIsModelTheory {L : Language} {M : Type u} [L.HasStructure M] : (L.theory M).IsModel M

@[simp]

theorem FirstOrder.Language.mem_theory {L : Language} {M : Type u} [L.HasStructure M] {p : L.Sentence} : p ∈ L.theory M ↔ M ⊨ₛ p

theorem FirstOrder.Language.theory_satisfiable (L : Language) (M : Type u) [L.HasStructure M] : Satisfiable.{u} (L.theory M)

def FirstOrder.Language.Structure.ulift {L : Language} (M : L.Structure) : L.Structure

Equations

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

theorem FirstOrder.Language.Structure.interp_ulift {L : Language} {n : ℕ} {t : L.Term n} {M : L.Structure} {ρ : Vec M.Dom n} : ⟦t⟧ₜ M.ulift.Dom, ULift.up ∘ ρ = { down := ⟦t⟧ₜ M.Dom, ρ }

theorem FirstOrder.Language.Structure.satisfy_ulift {L : Language} {n : ℕ} {p : L.Formula n} {M : L.Structure} {ρ : Vec M.Dom n} : M.ulift.Dom ⊨[ULift.up ∘ ρ] p ↔ M.Dom ⊨[ρ] p

theorem FirstOrder.Language.Entails.down {L : Language} {n : ℕ} {p : L.Formula n} {Γ : L.FormulaSet n} : Γ ⊨ p → Γ ⊨ p

theorem FirstOrder.Language.Satisfiable.up {L : Language} {n : ℕ} {Γ : L.FormulaSet n} : Satisfiable.{u} Γ → Satisfiable.{max u v} Γ

def FirstOrder.Language.Structure.ElementaryEquivalent {L : Language} (M : L.Structure) (N : L.Structure) : Prop

Two structures are elementary equivalent if they satisfy the same sentences.

Equations

• (M ≃ᴱ N) = ∀ (p : L.Sentence), M.Dom ⊨ₛ p ↔ N.Dom ⊨ₛ p

def FirstOrder.Language.Structure.«term_≃ᴱ_» : Lean.TrailingParserDescr

Equations

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

theorem FirstOrder.Language.Structure.ElementaryEquivalent.iff_theory_eq {L : Language} {M : L.Structure} {N : L.Structure} : M ≃ᴱ N ↔ L.theory M.Dom = L.theory N.Dom

structure FirstOrder.Language.Structure.Embedding {L : Language} (M : L.Structure) (N : L.Structure) extends M.Dom ↪ N.Dom : Type (max u_1 u_2)

• toFun : M.Dom → N.Dom
• inj' : Injective self.toFun
• on_func {m : ℕ} (f : L.Func m) (v : Vec M.Dom m) : self.toEmbedding (HasStructure.interpFunc f v) = HasStructure.interpFunc f (⇑self.toEmbedding ∘ v)
• on_rel {m : ℕ} (r : L.Rel m) (v : Vec M.Dom m) : HasStructure.interpRel r v ↔ HasStructure.interpRel r (⇑self.toEmbedding ∘ v)

def FirstOrder.Language.Structure.«term_↪ᴹ_» : Lean.TrailingParserDescr

Equations

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

instance FirstOrder.Language.Structure.Embedding.instCoeFunForallDom {L : Language} {M : L.Structure} {N : L.Structure} : CoeFun (M ↪ᴹ N) fun (x : M ↪ᴹ N) => M.Dom → N.Dom

Equations

• FirstOrder.Language.Structure.Embedding.instCoeFunForallDom = { coe := fun (x : M ↪ᴹ N) => ⇑x.toEmbedding }

def FirstOrder.Language.Structure.Embedding.refl {L : Language} {M : L.Structure} : M ↪ᴹ M

Equations

• FirstOrder.Language.Structure.Embedding.refl = { toEmbedding := Function.Embedding.refl M.Dom, on_func := ⋯, on_rel := ⋯ }

def FirstOrder.Language.Structure.Embedding.trans {L : Language} {M : L.Structure} {N : L.Structure} {R : L.Structure} (e₁ : M ↪ᴹ N) (e₂ : N ↪ᴹ R) : M ↪ᴹ R

Equations

• e₁.trans e₂ = { toEmbedding := e₁.trans e₂.toEmbedding, on_func := ⋯, on_rel := ⋯ }

theorem FirstOrder.Language.Structure.Embedding.on_term {L : Language} {n : ℕ} {M : L.Structure} {N : L.Structure} (e : M ↪ᴹ N) (t : L.Term n) (ρ : Vec M.Dom n) : e.toEmbedding (⟦t⟧ₜ M.Dom, ρ) = ⟦t⟧ₜ N.Dom, ⇑e.toEmbedding ∘ ρ

def FirstOrder.Language.Structure.Embedding.IsElementary {L : Language} {M : L.Structure} {N : L.Structure} (e : M ↪ᴹ N) : Prop

Equations

• e.IsElementary = ∀ {n : ℕ} (p : L.Formula n) (ρ : Vec M.Dom n), M.Dom ⊨[ρ] p ↔ N.Dom ⊨[⇑e.toEmbedding ∘ ρ] p

theorem FirstOrder.Language.Structure.Embedding.is_elementary_iff {L : Language} {M : L.Structure} {N : L.Structure} (e : M ↪ᴹ N) : e.IsElementary ↔ ∀ {n : ℕ} (p : L.Formula (n + 1)) (ρ : Vec M.Dom n), N.Dom ⊨[⇑e.toEmbedding ∘ ρ] ∃' p → ∃ (u : M.Dom), N.Dom ⊨[e.toEmbedding u ∷ᵥ ⇑e.toEmbedding ∘ ρ] p

Tarski–Vaught test.

structure FirstOrder.Language.Structure.Isomorphism {L : Language} (M : L.Structure) (N : L.Structure) extends M.Dom ≃ N.Dom : Type (max u_1 u_2)

• toFun : M.Dom → N.Dom
• invFun : N.Dom → M.Dom
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• on_func {m : ℕ} (f : L.Func m) (v : Vec M.Dom m) : self.toEquiv (HasStructure.interpFunc f v) = HasStructure.interpFunc f (⇑self.toEquiv ∘ v)
• on_rel {m : ℕ} (r : L.Rel m) (v : Vec M.Dom m) : HasStructure.interpRel r v ↔ HasStructure.interpRel r (⇑self.toEquiv ∘ v)

def FirstOrder.Language.Structure.«term_≃ᴹ_» : Lean.TrailingParserDescr

Equations

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

instance FirstOrder.Language.Structure.Isomorphism.instCoeFunForallDom {L : Language} {M : L.Structure} {N : L.Structure} : CoeFun (M ≃ᴹ N) fun (x : M ≃ᴹ N) => M.Dom → N.Dom

Equations

• FirstOrder.Language.Structure.Isomorphism.instCoeFunForallDom = { coe := fun (x : M ≃ᴹ N) => ⇑x.toEquiv }

def FirstOrder.Language.Structure.Isomorphism.refl {L : Language} {M : L.Structure} : M ≃ᴹ M

Equations

• FirstOrder.Language.Structure.Isomorphism.refl = { toEquiv := Equiv.refl M.Dom, on_func := ⋯, on_rel := ⋯ }

def FirstOrder.Language.Structure.Isomorphism.symm {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : N ≃ᴹ M

Equations

• i.symm = { toEquiv := i.symm, on_func := ⋯, on_rel := ⋯ }

def FirstOrder.Language.Structure.Isomorphism.trans {L : Language} {M : L.Structure} {N : L.Structure} {R : L.Structure} (i₁ : M ≃ᴹ N) (i₂ : N ≃ᴹ R) : M ≃ᴹ R

Equations

• i₁.trans i₂ = { toEquiv := i₁.trans i₂.toEquiv, on_func := ⋯, on_rel := ⋯ }

def FirstOrder.Language.Structure.Isomorphism.toEmbedding {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : M ↪ᴹ N

Equations

• i.toEmbedding = { toEmbedding := i.toEmbedding, on_func := ⋯, on_rel := ⋯ }

theorem FirstOrder.Language.Structure.Isomorphism.on_term {L : Language} {n : ℕ} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) (t : L.Term n) (ρ : Vec M.Dom n) : i.toEquiv (⟦t⟧ₜ M.Dom, ρ) = ⟦t⟧ₜ N.Dom, ⇑i.toEquiv ∘ ρ

theorem FirstOrder.Language.Structure.Isomorphism.on_formula {L : Language} {n : ℕ} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) (p : L.Formula n) (ρ : Vec M.Dom n) : M.Dom ⊨[ρ] p ↔ N.Dom ⊨[⇑i.toEquiv ∘ ρ] p

theorem FirstOrder.Language.Structure.Isomorphism.elementary_equivalent {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : M ≃ᴱ N