Documentation

Foundation.Modal.Hilbert

structure LO.Modal.InferenceRule (α : Type u_2) :
Type u_2

instance of inference rule

  • antecedents : List (LO.Modal.Formula α)
  • antecedents_nonempty : self.antecedents []

    Empty antecedent rule can be simply regarded as axiom rule. However, union of all these rules including to Hilbert.rules would be too complex for implementation and induction, so more than one antecedent is required.

  • consequence : LO.Modal.Formula α
Instances For
    theorem LO.Modal.InferenceRule.antecedents_nonempty {α : Type u_2} (self : LO.Modal.InferenceRule α) :
    self.antecedents []

    Empty antecedent rule can be simply regarded as axiom rule. However, union of all these rules including to Hilbert.rules would be too complex for implementation and induction, so more than one antecedent is required.

    @[reducible, inline]
    abbrev LO.Modal.InferenceRules (α : Type u_2) :
    Type u_2
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            structure LO.Modal.Hilbert (α : Type u_2) :
            Type u_2
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  inductive LO.Modal.Deduction {α : Type u_1} (Λ : LO.Modal.Hilbert α) :
                  Instances For
                    Equations
                    • LO.Modal.Deduction.instSystemFormulaHilbert = { Prf := LO.Modal.Deduction }
                    Equations
                    • LO.Modal.Deduction.instLukasiewiczHilbertFormula = LO.System.Lukasiewicz.mk
                    Equations
                    • LO.Modal.Deduction.instClassicalHilbertFormula = LO.System.Classical.mk
                    Equations
                    • LO.Modal.Deduction.instHasDiaDualityHilbertFormula = inferInstance
                    theorem LO.Modal.Deduction.maxm! {α : Type u_1} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} (h : p Ax(Λ)) :
                    Λ ⊢! p
                    Instances
                      theorem LO.Modal.Hilbert.HasNecessitation.has_necessitation {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasNecessitation] :
                      instance LO.Modal.Hilbert.instNecessitationFormulaOfHasNecessitation :
                      {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasNecessitation] → LO.System.Necessitation Λ
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances
                        theorem LO.Modal.Hilbert.HasLoebRule.has_loeb {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasLoebRule] :
                        instance LO.Modal.Hilbert.instLoebRuleFormulaOfHasLoebRule :
                        {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasLoebRule] → LO.System.LoebRule Λ
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances
                          theorem LO.Modal.Hilbert.HasHenkinRule.has_henkin {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasHenkinRule] :
                          instance LO.Modal.Hilbert.instHenkinRuleFormulaOfHasHenkinRule :
                          {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasHenkinRule] → LO.System.HenkinRule Λ
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances
                            theorem LO.Modal.Hilbert.HasNecOnly.has_necessitation_only {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasNecOnly] :
                            instance LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly :
                            {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [h : Λ.HasNecOnly] → Λ.HasNecessitation
                            Equations
                            • LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly = { has_necessitation := }
                            Instances
                              theorem LO.Modal.Hilbert.HasAxiomK.has_axiomK {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasAxiomK] :
                              instance LO.Modal.Hilbert.instHasAxiomKFormulaOfHasAxiomK :
                              {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasAxiomK] → LO.System.HasAxiomK Λ
                              Equations
                              noncomputable def LO.Modal.Deduction.inducition! {α : Type u_1} {Λ : LO.Modal.Hilbert α} {motive : (p : LO.Modal.Formula α) → Λ ⊢! pSort u_2} (hRules : (r : LO.Modal.InferenceRule α) → (hr : r Rl(Λ)) → (hant : ∀ {p : LO.Modal.Formula α}, p r.antecedentsΛ ⊢! p) → ({p : LO.Modal.Formula α} → (hp : p r.antecedents) → motive p )motive r.consequence ) (hMaxm : {p : LO.Modal.Formula α} → (h : p Ax(Λ)) → motive p ) (hMdp : {p q : LO.Modal.Formula α} → {hpq : Λ ⊢! p q} → {hp : Λ ⊢! p} → motive (p q) hpqmotive p hpmotive q ) (hImply₁ : {p q : LO.Modal.Formula α} → motive (p q p) ) (hImply₂ : {p q r : LO.Modal.Formula α} → motive ((p q r) (p q) p r) ) (hElimContra : {p q : LO.Modal.Formula α} → motive (LO.Axioms.ElimContra p q) ) {p : LO.Modal.Formula α} (d : Λ ⊢! p) :
                              motive p d
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                noncomputable def LO.Modal.Deduction.inducition_with_necOnly! {α : Type u_1} {Λ : LO.Modal.Hilbert α} [Λ.HasNecOnly] {motive : (p : LO.Modal.Formula α) → Λ ⊢! pProp} (hMaxm : ∀ {p : LO.Modal.Formula α} (h : p Ax(Λ)), motive p ) (hMdp : ∀ {p q : LO.Modal.Formula α} {hpq : Λ ⊢! p q} {hp : Λ ⊢! p}, motive (p q) hpqmotive p hpmotive q ) (hNec : ∀ {p : LO.Modal.Formula α} {hp : Λ ⊢! p}, motive p hpmotive (p) ) (hImply₁ : ∀ {p q : LO.Modal.Formula α}, motive (p q p) ) (hImply₂ : ∀ {p q r : LO.Modal.Formula α}, motive ((p q r) (p q) p r) ) (hElimContra : ∀ {p q : LO.Modal.Formula α}, motive (LO.Axioms.ElimContra p q) ) {p : LO.Modal.Formula α} (d : Λ ⊢! p) :
                                motive p d

                                Useful induction for normal modal Foundation.

                                Equations
                                • =
                                Instances For
                                  @[reducible, inline]
                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev LO.Modal.K {α : Type u_1} :
                                    Equations
                                    Instances For
                                      instance LO.Modal.instIsNormalK {α : Type u_1} :
                                      𝐊.IsNormal
                                      Equations
                                      • LO.Modal.instIsNormalK = LO.Modal.Hilbert.IsNormal.mk
                                      @[reducible, inline]
                                      abbrev LO.Modal.ExtK {α : Type u_1} (Ax : LO.Modal.Theory α) :
                                      Equations
                                      Instances For
                                        instance LO.Modal.instIsNormalExtK {α : Type u_1} {Ax : LO.Modal.Theory α} :
                                        (𝜿Ax).IsNormal
                                        Equations
                                        • LO.Modal.instIsNormalExtK = LO.Modal.Hilbert.IsNormal.mk
                                        theorem LO.Modal.Normal.maxm! {α : Type u_1} {Ax : LO.Modal.Theory α} {p : LO.Modal.Formula α} (h : p Ax) :
                                        @[reducible, inline]
                                        abbrev LO.Modal.ExtS4 {α : Type u_1} (Ax : LO.Modal.Theory α) :
                                        Equations
                                        Instances For
                                          Equations
                                          • LO.Modal.instS4HilbertFormulaExtS4 = LO.System.S4.mk
                                          @[simp]
                                          theorem LO.Modal.ExtS4.def_ax :
                                          ∀ {α : Type u_2} {Ax : LO.Modal.Theory α}, Ax(𝝈Ax) = 𝗞 𝗧 𝟰 Ax
                                          @[reducible, inline]
                                          abbrev LO.Modal.KT {α : Type u_1} :
                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev LO.Modal.KB {α : Type u_1} :
                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev LO.Modal.KD {α : Type u_1} :
                                              Equations
                                              Instances For
                                                Equations
                                                • LO.Modal.instKDHilbertFormulaKD = LO.System.KD.mk
                                                @[reducible, inline]
                                                abbrev LO.Modal.KP {α : Type u_1} :
                                                Equations
                                                Instances For
                                                  Equations
                                                  @[reducible, inline]
                                                  abbrev LO.Modal.KTB {α : Type u_1} :
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev LO.Modal.K4 {α : Type u_1} :
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • LO.Modal.instK4HilbertFormulaK4 = LO.System.K4.mk
                                                      @[reducible, inline]
                                                      abbrev LO.Modal.K5 {α : Type u_1} :
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev LO.Modal.S4 {α : Type u_1} :
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          • LO.Modal.instS4HilbertFormulaS4 = LO.System.S4.mk
                                                          @[reducible, inline]
                                                          abbrev LO.Modal.S4Dot2 {α : Type u_1} :
                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev LO.Modal.S4Dot3 {α : Type u_1} :
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev LO.Modal.S4Grz {α : Type u_1} :
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev LO.Modal.KT4B {α : Type u_1} :
                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]
                                                                    abbrev LO.Modal.S5 {α : Type u_1} :
                                                                    Equations
                                                                    Instances For
                                                                      Equations
                                                                      • LO.Modal.instS5HilbertFormulaS5 = LO.System.S5.mk
                                                                      @[reducible, inline]
                                                                      abbrev LO.Modal.S5Grz {α : Type u_1} :
                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          • LO.Modal.instS5HilbertFormulaS5Grz = LO.System.S5.mk
                                                                          Equations
                                                                          • LO.Modal.instGrzHilbertFormulaS5Grz = LO.System.Grz.mk
                                                                          @[reducible, inline]
                                                                          abbrev LO.Modal.Triv {α : Type u_1} :
                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            • LO.Modal.instTrivHilbertFormulaTriv = LO.System.Triv.mk
                                                                            @[reducible, inline]
                                                                            abbrev LO.Modal.Ver {α : Type u_1} :
                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              • LO.Modal.instVerHilbertFormulaVer = LO.System.Ver.mk
                                                                              @[reducible, inline]
                                                                              abbrev LO.Modal.GL {α : Type u_1} :
                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                • LO.Modal.instGLHilbertFormulaGL = LO.System.GL.mk
                                                                                @[reducible, inline]
                                                                                abbrev LO.Modal.Grz {α : Type u_1} :
                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  • LO.Modal.instGrzHilbertFormulaGrz = LO.System.Grz.mk
                                                                                  @[reducible, inline]
                                                                                  abbrev LO.Modal.K4H {α : Type u_1} :
                                                                                  Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                    • LO.Modal.instK4HHilbertFormulaK4H = LO.System.K4H.mk
                                                                                    @[reducible, inline]
                                                                                    abbrev LO.Modal.K4Loeb {α : Type u_1} :
                                                                                    Equations
                                                                                    Instances For
                                                                                      instance LO.Modal.instHasAxiomKK4Loeb {α : Type u_1} :
                                                                                      𝐊𝟒(𝐋).HasAxiomK
                                                                                      Equations
                                                                                      • LO.Modal.instHasAxiomKK4Loeb = { has_axiomK := }
                                                                                      instance LO.Modal.instHasNecessitationK4Loeb {α : Type u_1} :
                                                                                      𝐊𝟒(𝐋).HasNecessitation
                                                                                      Equations
                                                                                      • LO.Modal.instHasNecessitationK4Loeb = { has_necessitation := }
                                                                                      instance LO.Modal.instHasLoebRuleK4Loeb {α : Type u_1} :
                                                                                      𝐊𝟒(𝐋).HasLoebRule
                                                                                      Equations
                                                                                      • LO.Modal.instHasLoebRuleK4Loeb = { has_loeb := }
                                                                                      Equations
                                                                                      • LO.Modal.instK4LoebHilbertFormulaK4Loeb = LO.System.K4Loeb.mk
                                                                                      @[reducible, inline]
                                                                                      Equations
                                                                                      Instances For
                                                                                        instance LO.Modal.instHasAxiomKK4Henkin {α : Type u_1} :
                                                                                        𝐊𝟒(𝐇).HasAxiomK
                                                                                        Equations
                                                                                        • LO.Modal.instHasAxiomKK4Henkin = { has_axiomK := }
                                                                                        instance LO.Modal.instHasNecessitationK4Henkin {α : Type u_1} :
                                                                                        𝐊𝟒(𝐇).HasNecessitation
                                                                                        Equations
                                                                                        • LO.Modal.instHasNecessitationK4Henkin = { has_necessitation := }
                                                                                        instance LO.Modal.instHasHenkinRuleK4Henkin {α : Type u_1} :
                                                                                        𝐊𝟒(𝐇).HasHenkinRule
                                                                                        Equations
                                                                                        • LO.Modal.instHasHenkinRuleK4Henkin = { has_henkin := }
                                                                                        Equations
                                                                                        • LO.Modal.instK4HenkinHilbertFormulaK4Henkin = LO.System.K4Henkin.mk
                                                                                        @[reducible, inline]
                                                                                        abbrev LO.Modal.GLS {α : Type u_1} :

                                                                                        Solovey's Provability Logic of True Arithmetic. Remark necessitation is not permitted.

                                                                                        Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                          Equations
                                                                                          Equations
                                                                                          @[reducible, inline]
                                                                                          abbrev LO.Modal.N {α : Type u_1} :

                                                                                          Logic of Pure Necessitation

                                                                                          Equations
                                                                                          Instances For
                                                                                            instance LO.Modal.instHasNecOnlyN {α : Type u_1} :
                                                                                            𝐍.HasNecOnly
                                                                                            Equations
                                                                                            • LO.Modal.instHasNecOnlyN = { has_necessitation_only := }
                                                                                            theorem LO.Modal.normal_weakerThan_of_maxm {α : Type u_1} [DecidableEq α] {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [Λ₁.IsNormal] [Λ₂.IsNormal] (hMaxm : ∀ {p : LO.Modal.Formula α}, p Ax(Λ₁)Λ₂ ⊢! p) :
                                                                                            Λ₁ ≤ₛ Λ₂
                                                                                            theorem LO.Modal.normal_weakerThan_of_subset {α : Type u_1} [DecidableEq α] {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [Λ₁.IsNormal] [Λ₂.IsNormal] (hSubset : autoParam (Ax(Λ₁) Ax(Λ₂)) _auto✝) :
                                                                                            Λ₁ ≤ₛ Λ₂