Documentation

Foundation.Logic.Calculus

Sequent calculus and variants #

This file defines a characterization of Tait style calculus and Gentzen style calculus.

Main Definitions #

class LO.OneSided (F : outParam (Type u_1)) (K : Type u_2) :
Type (max (max u_1 u_2) (u_3 + 1))
Instances
    @[reducible, inline]
    abbrev LO.OneSided.Derivation₁ {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (p : F) :
    Type u_3
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.OneSided.Derivable {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (Δ : List F) :
      Equations
      Instances For
        @[reducible, inline]
        abbrev LO.OneSided.Derivable₁ {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (p : F) :
        Equations
        Instances For
          noncomputable def LO.OneSided.Derivable.get {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (Δ : List F) (h : 𝓚 ⟹! Δ) :
          𝓚 Δ
          Equations
          Instances For
            class LO.Tait (F : Type u_1) (K : Type u_2) [LO.LogicalConnective F] [Collection F K] extends LO.OneSided :
            Type (max (max u_1 u_2) (u_3 + 1))
            • Derivation : KList FType u_3
            • verum : (𝓚 : K) → (Δ : List F) → 𝓚 :: Δ
            • and : {𝓚 : K} → {p q : F} → {Δ : List F} → 𝓚 p :: Δ𝓚 q :: Δ𝓚 p q :: Δ
            • or : {𝓚 : K} → {p q : F} → {Δ : List F} → 𝓚 p :: q :: Δ𝓚 p q :: Δ
            • wk : {𝓚 : K} → {Δ Δ' : List F} → 𝓚 ΔΔ Δ'𝓚 Δ'
            • em : {𝓚 : K} → {p : F} → {Δ : List F} → p Δp Δ𝓚 Δ
            Instances
              class LO.Tait.Cut (F : Type u_1) (K : Type u_2) [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] :
              Type (max (max u_1 u_2) u_3)
              • cut : {𝓚 : K} → {Δ : List F} → {p : F} → 𝓚 p :: Δ𝓚 p :: Δ𝓚 Δ
              Instances
                class LO.Tait.Axiomatized (F : Type u_1) (K : Type u_2) [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] :
                Type (max (max u_1 u_2) u_3)
                • root : {𝓚 : K} → {p : F} → p 𝓚𝓚 ⟹. p
                • trans : {𝓚 𝓛 : K} → {Γ : List F} → ((q : F) → q 𝓚𝓛 ⟹. q)𝓚 Γ𝓛 Γ
                Instances
                  @[reducible, inline]
                  abbrev LO.OneSided.cast {F : Type u_1} {K : Type u_3} [LO.OneSided F K] {𝓚 : K} {Γ : List F} {Δ : List F} (d : 𝓚 Δ) (e : Δ = Γ) :
                  𝓚 Γ
                  Equations
                  Instances For
                    def LO.Tait.ofEq {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {Δ : List F} (b : 𝓚 Γ) (h : Γ = Δ) :
                    𝓚 Δ
                    Equations
                    Instances For
                      theorem LO.Tait.of_eq {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {Δ : List F} (b : 𝓚 ⟹! Γ) (h : Γ = Δ) :
                      𝓚 ⟹! Δ
                      def LO.Tait.verum' {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} (h : autoParam ( Γ) _auto✝) :
                      𝓚 Γ
                      Equations
                      Instances For
                        theorem LO.Tait.verum! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] (𝓚 : K) (Γ : List F) :
                        𝓚 ⟹! :: Γ
                        theorem LO.Tait.verum'! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} (h : Γ) :
                        𝓚 ⟹! Γ
                        theorem LO.Tait.and! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} {q : F} (hp : 𝓚 ⟹! p :: Γ) (hq : 𝓚 ⟹! q :: Γ) :
                        𝓚 ⟹! p q :: Γ
                        theorem LO.Tait.or! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} {q : F} (h : 𝓚 ⟹! p :: q :: Γ) :
                        𝓚 ⟹! p q :: Γ
                        theorem LO.Tait.wk! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {Δ : List F} (h : 𝓚 ⟹! Γ) (ss : Γ Δ) :
                        𝓚 ⟹! Δ
                        theorem LO.Tait.em! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} (hp : p Γ) (hn : p Γ) :
                        𝓚 ⟹! Γ
                        def LO.Tait.close {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} (p : F) (hp : autoParam (p Γ) _auto✝) (hn : autoParam (p Γ) _auto✝) :
                        𝓚 Γ
                        Equations
                        Instances For
                          theorem LO.Tait.close! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} (p : F) (hp : autoParam (p Γ) _auto✝) (hn : autoParam (p Γ) _auto✝) :
                          𝓚 ⟹! Γ
                          def LO.Tait.and' {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} {q : F} (h : p q Γ) (dp : 𝓚 p :: Γ) (dq : 𝓚 q :: Γ) :
                          𝓚 Γ
                          Equations
                          Instances For
                            def LO.Tait.or' {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} {q : F} (h : p q Γ) (dpq : 𝓚 p :: q :: Γ) :
                            𝓚 Γ
                            Equations
                            Instances For
                              def LO.Tait.wkTail {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p : F} (d : 𝓚 Γ) :
                              𝓚 p :: Γ
                              Equations
                              Instances For
                                def LO.Tait.rotate₁ {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p₁ : F} {p₂ : F} (d : 𝓚 p₂ :: p₁ :: Γ) :
                                𝓚 p₁ :: p₂ :: Γ
                                Equations
                                Instances For
                                  def LO.Tait.rotate₂ {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p₁ : F} {p₂ : F} {p₃ : F} (d : 𝓚 p₃ :: p₁ :: p₂ :: Γ) :
                                  𝓚 p₁ :: p₂ :: p₃ :: Γ
                                  Equations
                                  Instances For
                                    def LO.Tait.rotate₃ {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {𝓚 : K} {Γ : List F} {p₁ : F} {p₂ : F} {p₃ : F} {p₄ : F} (d : 𝓚 p₄ :: p₁ :: p₂ :: p₃ :: Γ) :
                                    𝓚 p₁ :: p₂ :: p₃ :: p₄ :: Γ
                                    Equations
                                    Instances For
                                      def LO.Tait.cut {F : Type u_1} {K : Type u_2} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [self : LO.Tait.Cut F K] {𝓚 : K} {Δ : List F} {p : F} :
                                      𝓚 p :: Δ𝓚 p :: Δ𝓚 Δ

                                      Alias of LO.Tait.Cut.cut.

                                      Equations
                                      Instances For
                                        def LO.Tait.root {F : Type u_1} {K : Type u_2} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [self : LO.Tait.Axiomatized F K] {𝓚 : K} {p : F} :
                                        p 𝓚𝓚 ⟹. p

                                        Alias of LO.Tait.Axiomatized.root.

                                        Equations
                                        Instances For
                                          theorem LO.Tait.cut! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] {Δ : List F} {p : F} [LO.Tait.Cut F K] {𝓚 : K} (hp : 𝓚 ⟹! p :: Δ) (hn : 𝓚 ⟹! p :: Δ) :
                                          𝓚 ⟹! Δ
                                          theorem LO.Tait.root! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {p : F} (h : p 𝓚) :
                                          𝓚 ⟹!. p
                                          def LO.Tait.byAxm {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {Γ : List F} (p : F) (h : p 𝓚) (hΓ : autoParam (p Γ) _auto✝) :
                                          𝓚 Γ
                                          Equations
                                          Instances For
                                            theorem LO.Tait.byAxm! {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {Γ : List F} (p : F) (h : p 𝓚) (hΓ : autoParam (p Γ) _auto✝) :
                                            𝓚 ⟹! Γ
                                            def LO.Tait.ofAxiomSubset {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {𝓛 : K} {Γ : List F} (h : 𝓚 𝓛) :
                                            𝓚 Γ𝓛 Γ
                                            Equations
                                            Instances For
                                              theorem LO.Tait.of_axiom_subset {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {𝓛 : K} {Γ : List F} (h : 𝓚 𝓛) :
                                              𝓚 ⟹! Γ𝓛 ⟹! Γ
                                              instance LO.Tait.system {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] :
                                              Equations
                                              • LO.Tait.system = { Prf := fun (x : K) (x_1 : F) => x ⟹. x_1 }
                                              Equations
                                              theorem LO.Tait.waekerThan_of_subset {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.Tait F K] [LO.Tait.Axiomatized F K] {𝓚 : K} {𝓛 : K} (h : 𝓚 𝓛) :
                                              𝓚 ≤ₛ 𝓛
                                              Equations
                                              theorem LO.Tait.provable_bot_iff_derivable_nil {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.DeMorgan F] [LO.Tait F K] [LO.Tait.Cut F K] {𝓚 : K} :
                                              𝓚 ⟹! [] 𝓚 ⊢!
                                              Equations
                                              instance LO.Tait.instClassical {F : Type u_1} {K : Type u_3} [LO.LogicalConnective F] [Collection F K] [LO.DeMorgan F] [LO.Tait F K] [LO.Tait.Cut F K] {𝓚 : K} :
                                              Equations
                                              • LO.Tait.instClassical = LO.System.Classical.mk