Documentation

Logic.FirstOrder.Interpretation

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)
domain_nonempty : T ⊨ ∃' LO.FirstOrder.Rew.emb.hom self.domain
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') :

T ⊨ ∃' LO.FirstOrder.Rew.emb.hom self.domain

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) :

LO.FirstOrder.Semisentence L 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 : ℕ} :

LO.FirstOrder.Semisentence L' n → LO.FirstOrder.Semisentence 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) :

ι.translationAux (∼p) = ∼ι.translationAux p

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 : ℕ} :

LO.FirstOrder.Semisentence L' n →ˡᶜ LO.FirstOrder.Semisentence 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) :

Equations

ι.Dom x = M ⊧/![x] ι.domain

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} :

ι.Dom x ↔ M ⊧/![x] ι.domain

@[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] :

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) :

(∀ (i : Fin k), ι.Dom (v i)) → ∃! y : M, ι.Dom y ∧ M ⊧/(y :> v) (ι.func f)

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) :

∃! y : ι.Sub M, M ⊧/(↑y :> fun (i : Fin k) => ↑(v i)) (ι.func f)

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) :

y = LO.FirstOrder.Structure.func f v ↔ M ⊧/(↑y :> fun (i : Fin k) => ↑(v i)) (ι.func f)

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} :

M ⊧/(↑y :> fun (i : Fin n) => ↑(x i)) (ι.varEquals t) ↔ y = LO.FirstOrder.Semiterm.valbm (ι.Sub M) x t

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} :

(M ⊧/fun (i : Fin n) => ↑(e i)) (ι.translation p) ↔ (ι.Sub M) ⊧/e p

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'} :

M ⊧/![] (ι.translation p) ↔ (ι.Sub M) ⊧/![] p

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] :

LO.FirstOrder.Interpretation T L

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))

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))

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) :

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))