Documentation

Foundation.IntProp.Deduction

structure LO.IntProp.Hilbert (α : Type u_1) :
Type u_1
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Instances
        Instances
          Instances
            inductive LO.IntProp.Deduction {α : Type u} (Λ : LO.IntProp.Hilbert α) :
            Instances For
              Equations
              • LO.IntProp.instSystemFormulaHilbert = { Prf := LO.IntProp.Deduction }
              Equations
              • LO.IntProp.instMinimalHilbertFormula = LO.System.Minimal.mk
              Equations
              Equations
              Equations
              Equations
              • LO.IntProp.instIntuitionisticHilbertFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk
              Equations
              • LO.IntProp.instClassicalHilbertFormulaOfIncludeDNE = LO.System.Classical.mk
              Equations
              • LO.IntProp.instClassicalHilbertFormulaOfIncludeEFQOfIncludeLEM = LO.System.Classical.mk
              theorem LO.IntProp.Deduction.eaxm! {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} (h : p Ax(Λ)) :
              Λ ⊢! p
              @[reducible, inline]
              Equations
              Instances For
                @[reducible, inline]
                Equations
                • LO.IntProp.Hilbert.Minimal = { axiomSet := }
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For
                    Equations
                    • LO.IntProp.Hilbert.instIncludeEFQIntuitionistic = { include_EFQ := }
                    Equations
                    • LO.IntProp.Hilbert.instIntuitionisticFormulaIntuitionistic = LO.System.Intuitionistic.mk
                    @[reducible, inline]
                    Equations
                    Instances For
                      Equations
                      • LO.IntProp.Hilbert.instIncludeLEMClassical = { include_LEM := }
                      Equations
                      • LO.IntProp.Hilbert.instIncludeEFQClassical = { include_EFQ := }
                      @[reducible, inline]
                      Equations
                      Instances For
                        instance LO.IntProp.Hilbert.instIncludeEFQKC {α : Type u} :
                        𝐊𝐂.IncludeEFQ
                        Equations
                        • LO.IntProp.Hilbert.instIncludeEFQKC = { include_EFQ := }
                        Equations
                        @[reducible, inline]
                        Equations
                        Instances For
                          instance LO.IntProp.Hilbert.instIncludeEFQLC {α : Type u} :
                          𝐋𝐂.IncludeEFQ
                          Equations
                          • LO.IntProp.Hilbert.instIncludeEFQLC = { include_EFQ := }
                          Equations
                          @[reducible, inline]
                          Equations
                          Instances For
                            @[reducible, inline]
                            Equations
                            • LO.IntProp.Hilbert.WeakClassical = { axiomSet := 𝗣𝗲 }
                            Instances For
                              noncomputable def LO.IntProp.Deduction.rec! {α : Type u} {Λ : LO.IntProp.Hilbert α} {motive : (a : LO.IntProp.Formula α) → Λ ⊢! aSort u_1} (eaxm : {p : LO.IntProp.Formula α} → (a : p Ax(Λ)) → motive p ) (mdp : {p q : LO.IntProp.Formula α} → {hpq : Λ ⊢! p q} → {hp : Λ ⊢! p} → motive (p q) hpqmotive p hpmotive q ) (verum : motive ) (imply₁ : {p q : LO.IntProp.Formula α} → motive (p q p) ) (imply₂ : {p q r : LO.IntProp.Formula α} → motive ((p q r) (p q) p r) ) (and₁ : {p q : LO.IntProp.Formula α} → motive (p q p) ) (and₂ : {p q : LO.IntProp.Formula α} → motive (p q q) ) (and₃ : {p q : LO.IntProp.Formula α} → motive (p q p q) ) (or₁ : {p q : LO.IntProp.Formula α} → motive (p p q) ) (or₂ : {p q : LO.IntProp.Formula α} → motive (q p q) ) (or₃ : {p q r : LO.IntProp.Formula α} → motive ((p r) (q r) p q r) ) (neg_equiv : {p : LO.IntProp.Formula α} → motive (LO.Axioms.NegEquiv p) ) {a : LO.IntProp.Formula α} (t : Λ ⊢! a) :
                              motive a t
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem LO.IntProp.weaker_than_of_subset_axiomset' {α : Type u} {Λ₁ : LO.IntProp.Hilbert α} {Λ₂ : LO.IntProp.Hilbert α} (hMaxm : ∀ {p : LO.IntProp.Formula α}, p Ax(Λ₁)Λ₂ ⊢! p) :
                                Λ₁ ≤ₛ Λ₂
                                theorem LO.IntProp.weaker_than_of_subset_axiomset {α : Type u} {Λ₁ : LO.IntProp.Hilbert α} {Λ₂ : LO.IntProp.Hilbert α} (hSubset : autoParam (Ax(Λ₁) Ax(Λ₂)) _auto✝) :
                                Λ₁ ≤ₛ Λ₂