Documentation

Foundation.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' yx = y
Instances For
    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))
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        Instances For
          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 kLO.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 kLO.FirstOrder.Semiterm L' Empty n) :
            ι.translation (LO.FirstOrder.Semiformula.nrel r v) = ι.translationRel r v
            Equations
            • ι.Dom x = M ⊧/![x] ι.domain
            Instances For
              @[reducible, inline]
              Equations
              • ι.Sub M = { x : M // ι.Dom x }
              Instances For
                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 kM) :
                (∀ (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)
                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 kLO.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
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Instances
                    @[reducible, inline]
                    Equations
                    Instances For