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)
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)
:
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₂}
:
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
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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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)
:
def
LO.FirstOrder.Translation.translate
{L₁ : Language}
{L₂ : Language}
[L₁.Eq]
[L₂.Eq]
{T : Theory L₁}
[𝐄𝐐 ⪯ T]
(π : Translation T L₂)
{ξ : Type u_3}
{n : ℕ}
:
Equations
- π.translate = { toTr := π.translateAux, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }
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]
:
Equations
- One or more equations did not get rendered due to their size.
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)
@[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}
:
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}
:
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}
:
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}
:
@[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₂}
:
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)”)
@[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₀ φ)
Instances
Equations
- LO.FirstOrder.«term_⊳_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊳_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊳ ") (Lean.ParserDescr.cat `term 51))
Equations
- LO.FirstOrder.«term_⊲_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊲_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊲ ") (Lean.ParserDescr.cat `term 51))
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 φ
def
LO.FirstOrder.Interpretation.ofWeakerThan
{L : Language}
[L.Eq]
(T U : Theory L)
[𝐄𝐐 ⪯ T]
[U ⪯ T]
:
Equations
- LO.FirstOrder.Interpretation.ofWeakerThan T U = { trln := LO.FirstOrder.Translation.id T, interpret_theory := ⋯ }
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_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}
:
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₁]
:
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₂)
:
Equations
- τ.comp π = { trln := LO.FirstOrder.Interpretation.compTranslation (LO.FirstOrder.Interpretation.trln T₃) π, interpret_theory := ⋯ }