Translation and interpretation, bi-interpretation

structure LO.FirstOrder.Translation {L₁ : Language} [L₁.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] (L₂ : Language) [L₂.Eq] : Type (max u_1 u_2)

• domain : Semisentence L₁ 1
• rel {k : ℕ} : L₂.Rel k → Semisentence L₁ k
• func {k : ℕ} : L₂.Func k → Semisentence L₁ (k + 1)
• domain_nonempty : T ⊢!. ∃' self.domain
• func_defined {k : ℕ} (f : L₂.Func k) : T ⊢!. ∀* ((Matrix.conj fun (i : Fin k) => self.domain/[Semiterm.bvar i]) ➝ ∃'! self.domain/[Semiterm.bvar 0] ⋏ self.func f)
• preserve_eq : T ⊢!. (“∀' ∀' (!(self.domain/[Semiterm.bvar 1]) → (!(self.domain/[Semiterm.bvar 0]) → (!((self.rel op(=))/[Semiterm.bvar 1, Semiterm.bvar 0]) ↔ !!(Semiterm.bvar 1) = !!(Semiterm.bvar 0))))”)

theorem LO.FirstOrder.Translation.ext {L₁ : Language} {inst✝ : L₁.Eq} {T : Theory L₁} {inst✝¹ : 𝐄𝐐 ⪯ T} {L₂ : Language} {inst✝² : L₂.Eq} {x y : Translation T L₂} (domain : x.domain = y.domain) (rel : @rel L₁ inst✝ T inst✝¹ L₂ inst✝² x = @rel L₁ inst✝ T inst✝¹ L₂ inst✝² y) (func : @func L₁ inst✝ T inst✝¹ L₂ inst✝² x = @func L₁ inst✝ T inst✝¹ L₂ inst✝² y) : x = y

theorem LO.FirstOrder.Translation.ext_iff {L₁ : Language} {inst✝ : L₁.Eq} {T : Theory L₁} {inst✝¹ : 𝐄𝐐 ⪯ T} {L₂ : Language} {inst✝² : L₂.Eq} {x y : Translation T L₂} : x = y ↔ x.domain = y.domain ∧ @rel L₁ inst✝ T inst✝¹ L₂ inst✝² x = @rel L₁ inst✝ T inst✝¹ L₂ inst✝² y ∧ @func L₁ inst✝ T inst✝¹ L₂ inst✝² x = @func L₁ inst✝ T inst✝¹ L₂ inst✝² y

def LO.FirstOrder.Translation.fal {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n : ℕ} (φ : Semiformula L₁ ξ (n + 1)) : Semiformula L₁ ξ n

Equations

• (∀_[π] φ) = ∀[(LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.emb) (π.domain/[LO.FirstOrder.Semiterm.bvar 0])] φ

def LO.FirstOrder.Translation.exs {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n : ℕ} (φ : Semiformula L₁ ξ (n + 1)) : Semiformula L₁ ξ n

Equations

• (∃_[π] φ) = ∃[(LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.emb) (π.domain/[LO.FirstOrder.Semiterm.bvar 0])] φ

def LO.FirstOrder.Translation.«term∀_[_]_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Translation.«term∃_[_]_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Translation.neg_fal {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_1} {n : ℕ} (φ : Semiformula L₁ ξ (n + 1)) : ∼(∀_[π] φ) = ∃_[π] ∼φ

@[simp]

theorem LO.FirstOrder.Translation.neg_exs {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_1} {n : ℕ} (φ : Semiformula L₁ ξ (n + 1)) : ∼(∃_[π] φ) = ∀_[π] ∼φ

def LO.FirstOrder.Translation.varEqual {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n : ℕ} : Semiterm L₂ ξ n → Semiformula L₁ ξ (n + 1)

Equations

• One or more equations did not get rendered due to their size.
• π.varEqual (LO.FirstOrder.Semiterm.bvar x_1) = (“!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.bvar x_1.succ)”)
• π.varEqual (LO.FirstOrder.Semiterm.fvar x_1) = (“!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.fvar x_1)”)

def LO.FirstOrder.Translation.translateRel {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n k : ℕ} (r : L₂.Rel k) (v : Fin k → Semiterm L₂ ξ n) : Semiformula L₁ ξ n

Equations

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

def LO.FirstOrder.Translation.translateAux {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n : ℕ} : Semiformula L₂ ξ n → Semiformula L₁ ξ n

Equations

• π.translateAux (LO.FirstOrder.Semiformula.rel r v) = π.translateRel r v
• π.translateAux (LO.FirstOrder.Semiformula.nrel r v) = ∼π.translateRel r v
• π.translateAux LO.FirstOrder.Semiformula.verum = ⊤
• π.translateAux LO.FirstOrder.Semiformula.falsum = ⊥
• π.translateAux (φ.and ψ) = π.translateAux φ ⋏ π.translateAux ψ
• π.translateAux (φ.or ψ) = π.translateAux φ ⋎ π.translateAux ψ
• π.translateAux φ.all = ∀_[π] π.translateAux φ
• π.translateAux φ.ex = ∃_[π] π.translateAux φ

theorem LO.FirstOrder.Translation.translateAux_neg {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_1} {n : ℕ} (φ : Semiformula L₂ ξ n) : π.translateAux (∼φ) = ∼π.translateAux φ

def LO.FirstOrder.Translation.translate {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {ξ : Type u_3} {n : ℕ} : Semiformula L₂ ξ n →ˡᶜ Semiformula L₁ ξ n

Equations

• π.translate = { toTr := π.translateAux, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.FirstOrder.Translation.translate_rel {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {ξ : Type u_1} {n k : ℕ} (R : L₂.Rel k) (v : Fin k → Semiterm L₂ ξ n) : π.translate (Semiformula.rel R v) = π.translateRel R v

@[simp]

theorem LO.FirstOrder.Translation.translate_nrel {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {ξ : Type u_1} {n k : ℕ} (R : L₂.Rel k) (v : Fin k → Semiterm L₂ ξ n) : π.translate (Semiformula.nrel R v) = ∼π.translateRel R v

@[simp]

theorem LO.FirstOrder.Translation.translate_all {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L₂ ξ (n + 1)) : π.translate (∀' φ) = ∀_[π] π.translate φ

@[simp]

theorem LO.FirstOrder.Translation.translate_ex {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L₂ ξ (n + 1)) : π.translate (∃' φ) = ∃_[π] π.translate φ

def LO.FirstOrder.Translation.Dom {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) {M : Type u_1} [Structure L₁ M] (x : M) : Prop

Equations

• π.Dom x = M ⊧/![x] π.domain

theorem LO.FirstOrder.Translation.dom_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] {x : M} : π.Dom x ↔ M ⊧/![x] π.domain

theorem LO.FirstOrder.Translation.domain_exists {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] : ∃ (x : M), π.Dom x

structure LO.FirstOrder.Translation.Model {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) (M : Type u_1) [Structure L₁ M] : Type u_1

• val : M
• dom : π.Dom ↑self

theorem LO.FirstOrder.Translation.Model.ext_iff {L₁ : Language} {L₂ : Language} {inst✝ : L₁.Eq} {inst✝¹ : L₂.Eq} {T : Theory L₁} {inst✝² : 𝐄𝐐 ⪯ T} {π : Translation T L₂} {M : Type u_1} {inst✝³ : Structure L₁ M} {x y : π.Model M} : x = y ↔ ↑x = ↑y

theorem LO.FirstOrder.Translation.Model.ext {L₁ : Language} {L₂ : Language} {inst✝ : L₁.Eq} {inst✝¹ : L₂.Eq} {T : Theory L₁} {inst✝² : 𝐄𝐐 ⪯ T} {π : Translation T L₂} {M : Type u_1} {inst✝³ : Structure L₁ M} {x y : π.Model M} (val : ↑x = ↑y) : x = y

instance LO.FirstOrder.Translation.instCoeOutModel {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] : CoeOut (π.Model M) M

Equations

• LO.FirstOrder.Translation.instCoeOutModel = { coe := LO.FirstOrder.Translation.Model.val }

@[simp]

theorem LO.FirstOrder.Translation.Model.pval_sub_domain {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] (x : π.Model M) : M ⊧/![↑x] π.domain

instance LO.FirstOrder.Translation.Model.instNonemptyOfModelsTheory {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] : Nonempty (π.Model M)

@[simp]

theorem LO.FirstOrder.Translation.Model.coe_mem_domain {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] (x : π.Model M) : π.Dom ↑x

@[simp]

theorem LO.FirstOrder.Translation.Model.val_mk {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] (x : M) (hx : π.Dom x) : ↑⟨x, hx⟩ = x

@[simp]

theorem LO.FirstOrder.Translation.Model.eta {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] (x : π.Model M) (h : π.Dom ↑x) : ⟨↑x, h⟩ = x

@[simp]

theorem LO.FirstOrder.Translation.Model.val_inj_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] {x y : π.Model M} : ↑x = ↑y ↔ x = y

@[simp]

theorem LO.FirstOrder.Translation.Model.val_mk_eq_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] {x y : M} {hx : π.Dom x} {hy : π.Dom y} : ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

@[simp]

theorem LO.FirstOrder.Translation.Model.eval_fal {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {φ : Semiformula L₁ ξ (n + 1)} : (Semiformula.Evalm M e ε) (∀_[π] φ) ↔ ∀ (x : π.Model M), (Semiformula.Evalm M (↑x :> e) ε) φ

@[simp]

theorem LO.FirstOrder.Translation.Model.eval_exs {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {φ : Semiformula L₁ ξ (n + 1)} : (Semiformula.Evalm M e ε) (∃_[π] φ) ↔ ∃ (x : π.Model M), (Semiformula.Evalm M (↑x :> e) ε) φ

theorem LO.FirstOrder.Translation.Model.func_existsUnique_on_dom {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} (f : L₂.Func k) (v : Fin k → M) : (∀ (i : Fin k), π.Dom (v i)) → ∃! y : M, π.Dom y ∧ M ⊧/(y :> v) (π.func f)

theorem LO.FirstOrder.Translation.Model.func_existsUnique {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} (f : L₂.Func k) (v : Fin k → π.Model M) : ∃! y : π.Model M, M ⊧/(↑y :> fun (i : Fin k) => ↑(v i)) (π.func f)

noncomputable instance LO.FirstOrder.Translation.Model.struc {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] (π : Translation T L₂) (M : Type u_1) [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] : Structure L₂ (π.Model M)

Equations

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

theorem LO.FirstOrder.Translation.Model.rel_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} (r : L₂.Rel k) (v : Fin k → π.Model M) : Structure.rel r v ↔ (M ⊧/fun (i : Fin k) => ↑(v i)) (π.rel r)

@[simp]

theorem LO.FirstOrder.Translation.Model.eq_iff' {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {a b : π.Model M} : M ⊧/![↑a, ↑b] (π.rel op(=)) ↔ a = b

@[simp]

theorem LO.FirstOrder.Translation.Model.eq_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] (v : Fin 2 → π.Model M) : Structure.rel op(=) v ↔ v 0 = v 1

instance LO.FirstOrder.Translation.Model.instEq {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] : Structure.Eq L₂ (π.Model M)

theorem LO.FirstOrder.Translation.Model.func_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} {f : L₂.Func k} {y : π.Model M} {v : Fin k → π.Model M} : y = Structure.func f v ↔ M ⊧/(↑y :> fun (i : Fin k) => ↑(v i)) (π.func f)

theorem LO.FirstOrder.Translation.Model.func_iff' {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} {f : L₂.Func k} {y : M} {v : Fin k → π.Model M} : y = ↑(Structure.func f v) ↔ π.Dom y ∧ M ⊧/(y :> fun (i : Fin k) => ↑(v i)) (π.func f)

@[simp]

theorem LO.FirstOrder.Translation.Model.eval_func {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {k : ℕ} (f : L₂.Func k) (v : Fin k → π.Model M) : M ⊧/(↑(Structure.func f v) :> fun (i : Fin k) => ↑(v i)) (π.func f)

theorem LO.FirstOrder.Translation.Model.eval_varEqual_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {ξ : Type u_2} {n : ℕ} {t : Semiterm L₂ ξ n} {ε : ξ → π.Model M} {y : π.Model M} {x : Fin n → π.Model M} : (Semiformula.Evalm M (↑y :> fun (i : Fin n) => ↑(x i)) fun (x : ξ) => ↑(ε x)) (π.varEqual t) ↔ y = Semiterm.valm (π.Model M) x ε t

theorem LO.FirstOrder.Translation.Model.eval_translateRel_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {ξ : Type u_2} {n k : ℕ} {ε : ξ → π.Model M} (e : Fin n → π.Model M) (R : L₂.Rel k) (v : Fin k → Semiterm L₂ ξ n) : (Semiformula.Evalm M (fun (i : Fin n) => ↑(e i)) fun (i : ξ) => ↑(ε i)) (π.translateRel R v) ↔ Structure.rel R fun (i : Fin k) => Semiterm.valm (π.Model M) e ε (v i)

theorem LO.FirstOrder.Translation.Model.eval_translate_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {ξ : Type u_2} {n : ℕ} {φ : Semiformula L₂ ξ n} {ε : ξ → π.Model M} {e : Fin n → π.Model M} : (Semiformula.Evalm M (fun (i : Fin n) => ↑(e i)) fun (i : ξ) => ↑(ε i)) (π.translate φ) ↔ (Semiformula.Evalm (π.Model M) e ε) φ

theorem LO.FirstOrder.Translation.Model.evalb_translate_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {n : ℕ} {φ : Semisentence L₂ n} {e : Fin n → π.Model M} : (M ⊧/fun (i : Fin n) => ↑(e i)) (π.translate φ) ↔ (π.Model M) ⊧/e φ

theorem LO.FirstOrder.Translation.Model.evalb_cons_translate_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {n : ℕ} {φ : Semisentence L₂ (n + 1)} {x : π.Model M} {e : Fin n → π.Model M} : M ⊧/(↑x :> fun (i : Fin n) => ↑(e i)) (π.translate φ) ↔ (π.Model M) ⊧/(x :> e) φ

theorem LO.FirstOrder.Translation.Model.evalb_singleton_translate_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {φ : Semisentence L₂ 1} {x : π.Model M} : M ⊧/![↑x] (π.translate φ) ↔ (π.Model M) ⊧/![x] φ

theorem LO.FirstOrder.Translation.Model.evalb_doubleton_translate_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {φ : Semisentence L₂ 2} {x y : π.Model M} : M ⊧/![↑x, ↑y] (π.translate φ) ↔ (π.Model M) ⊧/![x, y] φ

theorem LO.FirstOrder.Translation.Model.translate_iff₀ {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {σ : Sentence L₂} : M ⊧ₘ₀ π.translate σ ↔ π.Model M ⊧ₘ₀ σ

@[simp]

theorem LO.FirstOrder.Translation.Model.translate_close₀_iff {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {π : Translation T L₂} {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {φ : SyntacticFormula L₂} : M ⊧ₘ₀ π.translate (Semiformula.close₀ φ) ↔ π.Model M ⊧ₘ φ

def LO.FirstOrder.Translation.id {L₁ : Language} [L₁.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] : Translation T L₁

Equations

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

theorem LO.FirstOrder.Translation.id_func_def {L₁ : Language} [L₁.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] {a✝ : ℕ} {f : L₁.Func a✝} : (Translation.id T).func f = (“!!(Semiterm.bvar 0) = !!(Semiterm.func f fun (x : Fin a✝) => Semiterm.bvar x.succ)”)

theorem LO.FirstOrder.Translation.id_rel_def {L₁ : Language} [L₁.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] {a✝ : ℕ} {R : L₁.Rel a✝} : (Translation.id T).rel R = Semiformula.rel R fun (x : Fin a✝) => Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Translation.id_Dom {L₁ : Language} [L₁.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {M : Type u_1} [Structure L₁ M] (x : M) : (Translation.id T).Dom x

@[simp]

theorem LO.FirstOrder.Translation.id_val_eq {L₁ : Language} [L₁.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {ξ : Type u_2} {n : ℕ} {ε : ξ → (Translation.id T).Model M} {e : Fin n → (Translation.id T).Model M} {t : Semiterm L₁ ξ n} : ↑(Semiterm.valm ((Translation.id T).Model M) e ε t) = Semiterm.valm M (fun (x : Fin n) => ↑(e x)) (fun (x : ξ) => ↑(ε x)) t

@[simp]

theorem LO.FirstOrder.Translation.id_models_iff {L₁ : Language} [L₁.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {M : Type u_1} [Structure L₁ M] [Nonempty M] [M ⊧ₘ* T] [Structure.Eq L₁ M] {ξ : Type u_2} {n : ℕ} {ε : ξ → (Translation.id T).Model M} {e : Fin n → (Translation.id T).Model M} {φ : Semiformula L₁ ξ n} : (Semiformula.Evalm ((Translation.id T).Model M) e ε) φ ↔ (Semiformula.Evalm M (fun (x : Fin n) => ↑(e x)) fun (x : ξ) => ↑(ε x)) φ

class LO.FirstOrder.Interpretation {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] (U : Theory L₂) : Type (max u_1 u_2)

• trln : Translation T L₂
• interpret_theory (φ : SyntacticFormula L₂) : φ ∈ U → T ⊢!. (trln U).translate (Semiformula.close₀ φ)

def LO.FirstOrder.«term_⊳_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊳_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊳_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊳ ") (Lean.ParserDescr.cat `term 51))

@[reducible, inline]

abbrev LO.FirstOrder.InterpretedBy {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] (U : Theory L₂) (T : Theory L₁) [𝐄𝐐 ⪯ T] : Type (max u_1 u_2)

Equations

• (U ⊲ T) = (T ⊳ U)

def LO.FirstOrder.«term_⊲_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊲_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊲_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊲ ") (Lean.ParserDescr.cat `term 51))

class LO.FirstOrder.Biinterpretation {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] (U : Theory L₂) [𝐄𝐐 ⪯ U] : Type (max u_1 u_2)

• r : T ⊳ U
• l : T ⊲ U

def LO.FirstOrder.«term_⋈_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⋈_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⋈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 51))

@[reducible, inline]

abbrev LO.FirstOrder.Interpretation.translate {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {U : Theory L₂} (π : T ⊳ U) {ξ : Type u_3} {n : ℕ} (φ : Semiformula L₂ ξ n) : Semiformula L₁ ξ n

Equations

• π.translate φ = (LO.FirstOrder.Interpretation.trln U).translate φ

@[reducible, inline]

abbrev LO.FirstOrder.Interpretation.Model {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {U : Theory L₂} (π : T ⊳ U) (M : Type u_1) [Structure L₁ M] : Type u_1

Equations

• π.Model M = (LO.FirstOrder.Interpretation.trln U).Model M

instance LO.FirstOrder.Interpretation.model_models_theory {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {U : Theory L₂} (π : T ⊳ U) {M : Type v} [Nonempty M] [Structure L₁ M] [Structure.Eq L₁ M] (hT : M ⊧ₘ* T) : π.Model M ⊧ₘ* U

theorem LO.FirstOrder.Interpretation.of_provability {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {U : Theory L₂} (π : T ⊳ U) {φ : SyntacticFormula L₂} (h : U ⊢! φ) : T ⊢!. π.translate (Semiformula.close₀ φ)

theorem LO.FirstOrder.Interpretation.of_provability₀ {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T : Theory L₁} [𝐄𝐐 ⪯ T] {U : Theory L₂} (π : T ⊳ U) {σ : Sentence L₂} (h : U ⊢!. σ) : T ⊢!. π.translate σ

def LO.FirstOrder.Interpretation.ofWeakerThan {L : Language} [L.Eq] (T U : Theory L) [𝐄𝐐 ⪯ T] [U ⪯ T] : U ⊲ T

Equations

• LO.FirstOrder.Interpretation.ofWeakerThan T U = { trln := LO.FirstOrder.Translation.id T, interpret_theory := ⋯ }

instance LO.FirstOrder.Interpretation.refl {L : Language} [L.Eq] (T : Theory L) [𝐄𝐐 ⪯ T] : T ⊳ T

Equations

• LO.FirstOrder.Interpretation.refl T = LO.FirstOrder.Interpretation.ofWeakerThan T T

def LO.FirstOrder.Interpretation.compTranslation {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) : Translation T₁ L₃

Equations

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

@[simp]

theorem LO.FirstOrder.Interpretation.compTranslation_domain_def {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) : (compTranslation τ π).domain = (trln T₂).domain ⋏ π.translate τ.domain

@[simp]

theorem LO.FirstOrder.Interpretation.compTranslation_func_def {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] {k : ℕ} (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) (f : L₃.Func k) : (compTranslation τ π).func f = π.translate (τ.func f)

@[simp]

theorem LO.FirstOrder.Interpretation.compTranslation_rel_def {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] {k : ℕ} (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) (R : L₃.Rel k) : (compTranslation τ π).rel R = π.translate (τ.rel R)

theorem LO.FirstOrder.Interpretation.compTranslation_Dom_iff {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) {M : Type u_1} [Nonempty M] [Structure L₁ M] [Structure.Eq L₁ M] [M ⊧ₘ* T₁] {x : M} : (compTranslation τ π).Dom x ↔ ∃ (z : τ.Model (π.Model M)), x = ↑↑z

theorem LO.FirstOrder.Interpretation.val_compTranslation_Model_equiv {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) {M : Type u_1} [Nonempty M] [Structure L₁ M] [Structure.Eq L₁ M] [M ⊧ₘ* T₁] {ξ : Type u_2} {n : ℕ} {t : Semiterm L₃ ξ n} {ε : ξ → (compTranslation τ π).Model M} {ε' : ξ → τ.Model (π.Model M)} (hε : ∀ (x : ξ), ↑(ε x) = ↑↑(ε' x)) {e : Fin n → (compTranslation τ π).Model M} {e' : Fin n → τ.Model (π.Model M)} (he : ∀ (x : Fin n), ↑(e x) = ↑↑(e' x)) : ↑(Semiterm.valm ((compTranslation τ π).Model M) e ε t) = ↑↑(Semiterm.valm (τ.Model (π.Model M)) e' ε' t)

theorem LO.FirstOrder.Interpretation.eval_compTranslation_Model_equiv {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) {M : Type u_1} [Nonempty M] [Structure L₁ M] [Structure.Eq L₁ M] [M ⊧ₘ* T₁] {ξ : Type u_2} {n : ℕ} {φ : Semiformula L₃ ξ n} {ε : ξ → (compTranslation τ π).Model M} {ε' : ξ → τ.Model (π.Model M)} (hε : ∀ (x : ξ), ↑(ε x) = ↑↑(ε' x)) {e : Fin n → (compTranslation τ π).Model M} {e' : Fin n → τ.Model (π.Model M)} (he : ∀ (x : Fin n), ↑(e x) = ↑↑(e' x)) : (Semiformula.Evalm ((compTranslation τ π).Model M) e ε) φ ↔ (Semiformula.Evalm (τ.Model (π.Model M)) e' ε') φ

theorem LO.FirstOrder.Interpretation.compTranslation_Model_equiv {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : Translation T₂ L₃) (π : T₁ ⊳ T₂) {M : Type u_1} [Nonempty M] [Structure L₁ M] [Structure.Eq L₁ M] [M ⊧ₘ* T₁] : (compTranslation τ π).Model M ≡ₑ[L₃] τ.Model (π.Model M)

def LO.FirstOrder.Interpretation.comp {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} {T₃ : Theory L₃} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (τ : T₂ ⊳ T₃) (π : T₁ ⊳ T₂) : T₁ ⊳ T₃

Equations

• τ.comp π = { trln := LO.FirstOrder.Interpretation.compTranslation (LO.FirstOrder.Interpretation.trln T₃) π, interpret_theory := ⋯ }

instance LO.FirstOrder.Biinterpretation.refl {L₁ : Language} [L₁.Eq] (T : Theory L₁) [𝐄𝐐 ⪯ T] : T ⋈ T

Equations

• LO.FirstOrder.Biinterpretation.refl T = { r := LO.FirstOrder.Interpretation.refl T, l := LO.FirstOrder.Interpretation.refl T }

def LO.FirstOrder.Biinterpretation.symm {L₁ : Language} {L₂ : Language} [L₁.Eq] [L₂.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] (π : T₁ ⋈ T₂) : T₂ ⋈ T₁

Equations

• π.symm = { r := LO.FirstOrder.Biinterpretation.l, l := LO.FirstOrder.Biinterpretation.r }

def LO.FirstOrder.Biinterpretation.trans {L₁ : Language} {L₂ : Language} {L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theory L₁} {T₂ : Theory L₂} {T₃ : Theory L₃} [𝐄𝐐 ⪯ T₁] [𝐄𝐐 ⪯ T₂] [𝐄𝐐 ⪯ T₃] (π : T₁ ⋈ T₂) (τ : T₂ ⋈ T₃) : T₁ ⋈ T₃

Equations

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