theorem
LO.FirstOrder.Interpretation.ext_iff
{L : LO.FirstOrder.Language}
:
∀ {inst : L.Eq} {T : LO.FirstOrder.Theory L} {inst_1 : 𝐄𝐐 ≼ T} {L' : LO.FirstOrder.Language}
(x y : LO.FirstOrder.Interpretation T L'),
x = y ↔ x.domain = y.domain ∧ @LO.FirstOrder.Interpretation.rel L inst T inst_1 L' x = @LO.FirstOrder.Interpretation.rel L inst T inst_1 L' y ∧ @LO.FirstOrder.Interpretation.func L inst T inst_1 L' x = @LO.FirstOrder.Interpretation.func L inst T inst_1 L' y
theorem
LO.FirstOrder.Interpretation.ext
{L : LO.FirstOrder.Language}
:
∀ {inst : L.Eq} {T : LO.FirstOrder.Theory L} {inst_1 : 𝐄𝐐 ≼ T} {L' : LO.FirstOrder.Language}
(x y : LO.FirstOrder.Interpretation T L'),
x.domain = y.domain →
@LO.FirstOrder.Interpretation.rel L inst T inst_1 L' x = @LO.FirstOrder.Interpretation.rel L inst T inst_1 L' y →
@LO.FirstOrder.Interpretation.func L inst T inst_1 L' x = @LO.FirstOrder.Interpretation.func L inst T inst_1 L' y →
x = y
structure
LO.FirstOrder.Interpretation
{L : LO.FirstOrder.Language}
[L.Eq]
(T : LO.FirstOrder.Theory L)
[𝐄𝐐 ≼ T]
(L' : LO.FirstOrder.Language)
:
Type (max u_1 u_2)
- domain : LO.FirstOrder.Semisentence L 1
- rel : {k : ℕ} → L'.Rel k → LO.FirstOrder.Semisentence L k
- func : {k : ℕ} → L'.Func k → LO.FirstOrder.Semisentence L (k + 1)
- func_defined : ∀ {k : ℕ} (f : L'.Func k), T ⊨ ∀* ((Matrix.conj fun (i : Fin k) => (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar i]).hom (LO.FirstOrder.Rew.emb.hom self.domain)) ➝ ∃'! (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom (LO.FirstOrder.Rew.emb.hom self.domain) ⋏ LO.FirstOrder.Rew.emb.hom (self.func f))
Instances For
theorem
LO.FirstOrder.Interpretation.domain_nonempty
{L : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{L' : LO.FirstOrder.Language}
(self : LO.FirstOrder.Interpretation T L')
:
theorem
LO.FirstOrder.Interpretation.func_defined
{L : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{L' : LO.FirstOrder.Language}
(self : LO.FirstOrder.Interpretation T L')
{k : ℕ}
(f : L'.Func k)
:
T ⊨ ∀* ((Matrix.conj fun (i : Fin k) =>
(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar i]).hom (LO.FirstOrder.Rew.emb.hom self.domain)) ➝ ∃'! (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom (LO.FirstOrder.Rew.emb.hom self.domain) ⋏ LO.FirstOrder.Rew.emb.hom (self.func f))
def
LO.FirstOrder.Interpretation.varEquals
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
:
LO.FirstOrder.Semiterm L' Empty n → LO.FirstOrder.Semisentence L (n + 1)
Equations
- One or more equations did not get rendered due to their size.
- ι.varEquals (LO.FirstOrder.Semiterm.bvar x_1) = (“!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.bvar x_1.succ)”)
Instances For
def
LO.FirstOrder.Interpretation.translationRel
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
{k : ℕ}
(r : L'.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L' Empty n)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Interpretation.translationAux
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
:
Equations
- ι.translationAux (LO.FirstOrder.Semiformula.rel r v) = ι.translationRel r v
- ι.translationAux (LO.FirstOrder.Semiformula.nrel r v) = ∼ι.translationRel r v
- ι.translationAux LO.FirstOrder.Semiformula.verum = ⊤
- ι.translationAux LO.FirstOrder.Semiformula.falsum = ⊥
- ι.translationAux (LO.FirstOrder.Semiformula.and p q) = ι.translationAux p ⋏ ι.translationAux q
- ι.translationAux (LO.FirstOrder.Semiformula.or p q) = ι.translationAux p ⋎ ι.translationAux q
- ι.translationAux (LO.FirstOrder.Semiformula.all p) = ∀[(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom ι.domain] ι.translationAux p
- ι.translationAux (LO.FirstOrder.Semiformula.ex p) = ∃[(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom ι.domain] ι.translationAux p
Instances For
theorem
LO.FirstOrder.Interpretation.translationAux_neg
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
(p : LO.FirstOrder.Semisentence L' n)
:
def
LO.FirstOrder.Interpretation.translation
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
:
Equations
- ι.translation = { toTr := ι.translationAux, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }
Instances For
@[simp]
theorem
LO.FirstOrder.Interpretation.translation_rel
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
{k : ℕ}
(r : L'.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L' Empty n)
:
ι.translation (LO.FirstOrder.Semiformula.rel r v) = ι.translationRel r v
@[simp]
theorem
LO.FirstOrder.Interpretation.translation_nrel
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
{k : ℕ}
(r : L'.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L' Empty n)
:
ι.translation (LO.FirstOrder.Semiformula.nrel r v) = ∼ι.translationRel r v
@[simp]
theorem
LO.FirstOrder.Interpretation.translation_all
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
(p : LO.FirstOrder.Semisentence L' (n + 1))
:
ι.translation (∀' p) = ∀[(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom ι.domain] ι.translation p
@[simp]
theorem
LO.FirstOrder.Interpretation.translation_ex
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{n : ℕ}
(p : LO.FirstOrder.Semisentence L' (n + 1))
:
ι.translation (∃' p) = ∃[(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom ι.domain] ι.translation p
def
LO.FirstOrder.Interpretation.Dom
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
{M : Type u}
[s : LO.FirstOrder.Structure L M]
(x : M)
:
Instances For
theorem
LO.FirstOrder.Interpretation.dom_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[s : LO.FirstOrder.Structure L M]
{x : M}
:
@[reducible, inline]
abbrev
LO.FirstOrder.Interpretation.Sub
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[s : LO.FirstOrder.Structure L M]
:
Type u
Equations
- ι.Sub M = { x : M // ι.Dom x }
Instances For
@[simp]
theorem
LO.FirstOrder.Interpretation.pval_sub_domain
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[s : LO.FirstOrder.Structure L M]
(x : ι.Sub M)
:
M ⊧/![↑x] ι.domain
theorem
LO.FirstOrder.Interpretation.sub_exists
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[M ⊧ₘ* T]
:
∃ (x : M), ι.Dom x
theorem
LO.FirstOrder.Interpretation.func_existsUnique_on_dom
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{k : ℕ}
(f : L'.Func k)
(v : Fin k → M)
:
theorem
LO.FirstOrder.Interpretation.func_existsUnique
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(ι : LO.FirstOrder.Interpretation T L')
(M : Type u)
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{k : ℕ}
(f : L'.Func k)
(v : Fin k → ι.Sub M)
:
instance
LO.FirstOrder.Interpretation.sub_nonempty
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[M ⊧ₘ* T]
:
Nonempty (ι.Sub M)
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.Interpretation.subStructure
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
:
LO.FirstOrder.Structure L' (ι.Sub M)
Equations
- One or more equations did not get rendered due to their size.
theorem
LO.FirstOrder.Interpretation.sub_rel_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{k : ℕ}
(r : L'.Rel k)
(v : Fin k → ι.Sub M)
:
LO.FirstOrder.Structure.rel r v ↔ (M ⊧/fun (i : Fin k) => ↑(v i)) (ι.rel r)
theorem
LO.FirstOrder.Interpretation.sub_func_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{k : ℕ}
(f : L'.Func k)
(y : ι.Sub M)
(v : Fin k → ι.Sub M)
:
theorem
LO.FirstOrder.Interpretation.eval_varEquals_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{n : ℕ}
{t : LO.FirstOrder.Semiterm L' Empty n}
{y : ι.Sub M}
{x : Fin n → ι.Sub M}
:
theorem
LO.FirstOrder.Interpretation.eval_translationRel_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{n : ℕ}
{k : ℕ}
(e : Fin n → ι.Sub M)
(r : L'.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L' Empty n)
:
(M ⊧/fun (i : Fin n) => ↑(e i)) (ι.translationRel r v) ↔ LO.FirstOrder.Structure.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.valbm (ι.Sub M) e (v i)
theorem
LO.FirstOrder.Interpretation.eval_translation_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{n : ℕ}
{p : LO.FirstOrder.Semisentence L' n}
{e : Fin n → ι.Sub M}
:
theorem
LO.FirstOrder.Interpretation.eval_translation_iff₀
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{p : LO.FirstOrder.Sentence L'}
:
theorem
LO.FirstOrder.Interpretation.models_translation_iff
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{ι : LO.FirstOrder.Interpretation T L'}
{M : Type u}
[Nonempty M]
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
[M ⊧ₘ* T]
{p : LO.FirstOrder.SyntacticFormula L'}
:
M ⊧ₘ LO.FirstOrder.Rew.emb.hom (ι.translation (LO.FirstOrder.Semiformula.close₀ p)) ↔ ι.Sub M ⊧ₘ p
def
LO.FirstOrder.Interpretation.id
{L : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
LO.FirstOrder.TheoryInterpretation
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
(T : LO.FirstOrder.Theory L)
[𝐄𝐐 ≼ T]
(U : LO.FirstOrder.Theory L')
:
Type u_1
- interpretation : LO.FirstOrder.Interpretation T L'
- interpret_theory : ∀ p ∈ U, T ⊨ LO.FirstOrder.Rew.emb.hom ((LO.FirstOrder.TheoryInterpretation.interpretation U).translation (LO.FirstOrder.Semiformula.close₀ p))
Instances
theorem
LO.FirstOrder.TheoryInterpretation.interpret_theory
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{U : LO.FirstOrder.Theory L'}
[self : T ⊳ U]
(p : LO.FirstOrder.SyntacticFormula L')
:
p ∈ U →
T ⊨ LO.FirstOrder.Rew.emb.hom
((LO.FirstOrder.TheoryInterpretation.interpretation U).translation (LO.FirstOrder.Semiformula.close₀ p))
Equations
- LO.FirstOrder.«term_⊳_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊳_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊳ ") (Lean.ParserDescr.cat `term 51))
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.TheoryInterpretation.translation
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{U : LO.FirstOrder.Theory L'}
(ι : T ⊳ U)
{n : ℕ}
(p : LO.FirstOrder.Semisentence L' n)
:
Equations
- ι.translation p = (LO.FirstOrder.TheoryInterpretation.interpretation U).translation p
Instances For
theorem
LO.FirstOrder.TheoryInterpretation.sub_models_theory
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{U : LO.FirstOrder.Theory L'}
(ι : T ⊳ U)
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
(hT : M ⊧ₘ* T)
:
(LO.FirstOrder.TheoryInterpretation.interpretation U).Sub M ⊧ₘ* U
theorem
LO.FirstOrder.TheoryInterpretation.theorem_translation
{L : LO.FirstOrder.Language}
{L' : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{U : LO.FirstOrder.Theory L'}
(ι : T ⊳ U)
{p : LO.FirstOrder.SyntacticFormula L'}
(h : U ⊨ p)
:
T ⊨ ↑(ι.translation (LO.FirstOrder.Semiformula.close₀ p))