Documentation

Foundation.FirstOrder.Completeness.SubLanguage

def LO.FirstOrder.Language.subLanguage (L : LO.FirstOrder.Language) (pfunc : (k : ) → L.Func kProp) (prel : (k : ) → L.Rel kProp) :
Equations
  • L.subLanguage pfunc prel = { Func := fun (k : ) => Subtype (pfunc k), Rel := fun (k : ) => Subtype (prel k) }
Instances For
    def LO.FirstOrder.Language.ofSubLanguage (L : LO.FirstOrder.Language) {pf : (k : ) → L.Func kProp} {pr : (k : ) → L.Rel kProp} :
    (L.subLanguage pf pr).Hom L
    Equations
    • L.ofSubLanguage = { func := fun {k : } => Subtype.val, rel := fun {k : } => Subtype.val }
    Instances For
      @[simp]
      theorem LO.FirstOrder.Language.ofSubLanguage_onFunc (L : LO.FirstOrder.Language) :
      ∀ {pfunc : (k : ) → L.Func kProp} {prel : (k : ) → L.Rel kProp} {a : } {p : (L.subLanguage pfunc prel).Func a}, L.ofSubLanguage.func p = p
      @[simp]
      theorem LO.FirstOrder.Language.ofSubLanguage_onRel (L : LO.FirstOrder.Language) :
      ∀ {pfunc : (k : ) → L.Func kProp} {prel : (k : ) → L.Rel kProp} {a : } {p : (L.subLanguage pfunc prel).Rel a}, L.ofSubLanguage.rel p = p
      def LO.FirstOrder.Semiterm.lang {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } :
      LO.FirstOrder.Semiterm L μ nFinset ((k : ) × L.Func k)
      Equations
      Instances For
        @[simp]
        theorem LO.FirstOrder.Semiterm.lang_func {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } {k : } (f : L.Func k) (v : Fin kLO.FirstOrder.Semiterm L μ n) :
        k, f (LO.FirstOrder.Semiterm.func f v).lang
        theorem LO.FirstOrder.Semiterm.lang_func_ss {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } {k : } (f : L.Func k) (v : Fin kLO.FirstOrder.Semiterm L μ n) (i : Fin k) :
        (v i).lang (LO.FirstOrder.Semiterm.func f v).lang
        def LO.FirstOrder.Semiterm.toSubLanguage' {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } (pf : (k : ) → L.Func kProp) (pr : (k : ) → L.Rel kProp) (t : LO.FirstOrder.Semiterm L μ n) :
        (∀ (k : ) (f : L.Func k), k, f t.langpf k f)LO.FirstOrder.Semiterm (L.subLanguage pf pr) μ n
        Equations
        Instances For
          @[simp]
          theorem LO.FirstOrder.Semiterm.lMap_toSubLanguage' {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } (pf : (k : ) → L.Func kProp) (pr : (k : ) → L.Rel kProp) (t : LO.FirstOrder.Semiterm L μ n) (h : ∀ (k : ) (f : L.Func k), k, f t.langpf k f) :
          noncomputable def LO.FirstOrder.Semiformula.langFunc {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } :
          LO.FirstOrder.Semiformula L μ nFinset ((k : ) × L.Func k)
          Equations
          • LO.FirstOrder.Semiformula.verum.langFunc =
          • LO.FirstOrder.Semiformula.falsum.langFunc =
          • (LO.FirstOrder.Semiformula.rel a v).langFunc = Finset.univ.biUnion fun (i : Fin arity) => (v i).lang
          • (LO.FirstOrder.Semiformula.nrel a v).langFunc = Finset.univ.biUnion fun (i : Fin arity) => (v i).lang
          • (p.and q).langFunc = p.langFunc q.langFunc
          • (p.or q).langFunc = p.langFunc q.langFunc
          • p.all.langFunc = p.langFunc
          • p.ex.langFunc = p.langFunc
          Instances For
            noncomputable def LO.FirstOrder.Semiformula.langRel {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } :
            LO.FirstOrder.Semiformula L μ nFinset ((k : ) × L.Rel k)
            Equations
            Instances For
              theorem LO.FirstOrder.Semiformula.langFunc_rel_ss {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } {k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L μ n) (i : Fin k) :
              (v i).lang (LO.FirstOrder.Semiformula.rel r v).langFunc
              def LO.FirstOrder.Semiformula.toSubLanguage' {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} (pf : (k : ) → L.Func kProp) (pr : (k : ) → L.Rel kProp) {n : } (p : LO.FirstOrder.Semiformula L μ n) :
              (∀ (k : ) (f : L.Func k), k, f p.langFuncpf k f)(∀ (k : ) (r : L.Rel k), k, r p.langRelpr k r)LO.FirstOrder.Semiformula (L.subLanguage pf pr) μ n
              Equations
              Instances For
                @[simp]
                theorem LO.FirstOrder.Semiformula.lMap_toSubLanguage' {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} (pf : (k : ) → L.Func kProp) (pr : (k : ) → L.Rel kProp) {n : } (p : LO.FirstOrder.Semiformula L μ n) (hf : ∀ (k : ) (f : L.Func k), k, f p.langFuncpf k f) (hr : ∀ (k : ) (r : L.Rel k), k, r p.langRelpr k r) :
                noncomputable def LO.FirstOrder.Semiformula.languageFuncIndexed {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } (p : LO.FirstOrder.Semiformula L μ n) (k : ) :
                Finset (L.Func k)
                Equations
                • p.languageFuncIndexed k = p.langFunc.preimage (Sigma.mk k)
                Instances For
                  noncomputable def LO.FirstOrder.Semiformula.languageRelIndexed {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } (p : LO.FirstOrder.Semiformula L μ n) (k : ) :
                  Finset (L.Rel k)
                  Equations
                  • p.languageRelIndexed k = p.langRel.preimage (Sigma.mk k)
                  Instances For
                    @[reducible, inline]
                    abbrev LO.FirstOrder.Semiformula.languageFinset {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } (Γ : Finset (LO.FirstOrder.Semiformula L μ n)) :
                    Equations
                    Instances For
                      noncomputable instance LO.FirstOrder.Semiformula.instFintypeFuncLanguageFinset {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } (Γ : Finset (LO.FirstOrder.Semiformula L μ n)) (k : ) :
                      Equations
                      noncomputable instance LO.FirstOrder.Semiformula.instFintypeRelLanguageFinset {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } (Γ : Finset (LO.FirstOrder.Semiformula L μ n)) (k : ) :
                      Equations
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        instance LO.FirstOrder.Structure.subLanguageStructure {L : LO.FirstOrder.Language} {pf : (k : ) → L.Func kProp} {pr : (k : ) → L.Rel kProp} {M : Type w} (s : LO.FirstOrder.Structure L M) :
                        LO.FirstOrder.Structure (L.subLanguage pf pr) M
                        Equations
                        noncomputable def LO.FirstOrder.Structure.extendStructure {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) {M : Type w} [Nonempty M] (s : LO.FirstOrder.Structure L₁ M) :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem LO.FirstOrder.Structure.extendStructure.func {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) {M : Type u} [Nonempty M] (s₁ : LO.FirstOrder.Structure L₁ M) {k : } (injf : Function.Injective Φ.func) (f₁ : L₁.Func k) (v : Fin kM) :
                          theorem LO.FirstOrder.Structure.extendStructure.rel {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) {M : Type u} [Nonempty M] (s₁ : LO.FirstOrder.Structure L₁ M) {k : } (injr : Function.Injective Φ.rel) (r₁ : L₁.Rel k) (v : Fin kM) :
                          theorem LO.FirstOrder.Structure.extendStructure.val_lMap {μ : Type u_1} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) {M : Type u} [Nonempty M] {n : } (e : Fin nM) (ε : μM) (injf : ∀ (k : ), Function.Injective Φ.func) (s₁ : LO.FirstOrder.Structure L₁ M) (t : LO.FirstOrder.Semiterm L₁ μ n) :
                          theorem LO.FirstOrder.Structure.extendStructure.eval_lMap {μ : Type u_1} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) (injf : ∀ (k : ), Function.Injective Φ.func) (injr : ∀ (k : ), Function.Injective Φ.rel) {M : Type u} [Nonempty M] (s₁ : LO.FirstOrder.Structure L₁ M) {n : } (e : Fin nM) (ε : μM) {p : LO.FirstOrder.Semiformula L₁ μ n} :
                          theorem LO.FirstOrder.Structure.extendStructure.models_lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) (injf : ∀ (k : ), Function.Injective Φ.func) (injr : ∀ (k : ), Function.Injective Φ.rel) {M : Type u} [Nonempty M] (s₁ : LO.FirstOrder.Structure L₁ M) (p : LO.FirstOrder.SyntacticFormula L₁) :