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} [OneSided F K] (𝓚 : K) (φ : F) :
    Type u_3
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.OneSided.Derivable {F : Type u_1} {K : Type u_2} [OneSided F K] (𝓚 : K) (Δ : List F) :
      Equations
      Instances For
        @[reducible, inline]
        abbrev LO.OneSided.Derivable₁ {F : Type u_1} {K : Type u_2} [OneSided F K] (𝓚 : K) (φ : F) :
        Equations
        Instances For
          noncomputable def LO.OneSided.Derivable.get {F : Type u_1} {K : Type u_2} [OneSided F K] (𝓚 : K) (Δ : List F) (h : 𝓚 ⟹! Δ) :
          𝓚 Δ
          Equations
          Instances For
            class LO.Tait (F : Type u_1) (K : Type u_2) [LogicalConnective F] [DeMorgan F] [Collection F K] extends LO.OneSided F K :
            Type (max (max u_1 u_2) (u_3 + 1))
            Instances
              class LO.Tait.Cut (F : Type u_1) (K : Type u_2) [LogicalConnective F] [DeMorgan F] [Collection F K] [Tait F K] :
              Type (max (max u_1 u_2) u_3)
              Instances
                class LO.Tait.Axiomatized (F : Type u_1) (K : Type u_2) [LogicalConnective F] [DeMorgan F] [Collection F K] [Tait F K] :
                Type (max (max u_1 u_2) u_3)
                • root {𝓚 : K} {φ : F} : φ 𝓚𝓚 ⟹. φ
                • trans {𝓚 𝓛 : K} {Γ : List F} : ((ψ : F) → ψ 𝓚𝓛 ⟹. ψ)𝓚 Γ𝓛 Γ
                Instances
                  @[reducible, inline]
                  abbrev LO.OneSided.cast {F : Type u_1} {K : Type u_3} [OneSided F K] {𝓚 : K} {Γ Δ : List F} (d : 𝓚 Δ) (e : Δ = Γ) :
                  𝓚 Γ
                  Equations
                  Instances For
                    def LO.Tait.ofEq {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ Δ : List F} (b : 𝓚 Γ) (h : Γ = Δ) :
                    𝓚 Δ
                    Equations
                    Instances For
                      theorem LO.Tait.of_eq {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ Δ : List F} (b : 𝓚 ⟹! Γ) (h : Γ = Δ) :
                      𝓚 ⟹! Δ
                      def LO.Tait.verum' {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} (h : Γ := by simp) :
                      𝓚 Γ
                      Equations
                      Instances For
                        theorem LO.Tait.verum! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] (𝓚 : K) (Γ : List F) :
                        𝓚 ⟹! :: Γ
                        theorem LO.Tait.verum'! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} (h : Γ) :
                        𝓚 ⟹! Γ
                        theorem LO.Tait.and! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ ψ : F} (hp : 𝓚 ⟹! φ :: Γ) (hq : 𝓚 ⟹! ψ :: Γ) :
                        𝓚 ⟹! φ ψ :: Γ
                        theorem LO.Tait.or! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ ψ : F} (h : 𝓚 ⟹! φ :: ψ :: Γ) :
                        𝓚 ⟹! φ ψ :: Γ
                        theorem LO.Tait.wk! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ Δ : List F} (h : 𝓚 ⟹! Γ) (ss : Γ Δ) :
                        𝓚 ⟹! Δ
                        theorem LO.Tait.em! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ : F} (hp : φ Γ) (hn : φ Γ) :
                        𝓚 ⟹! Γ
                        def LO.Tait.close {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} (φ : F) (hp : φ Γ := by simp) (hn : φ Γ := by simp) :
                        𝓚 Γ
                        Equations
                        Instances For
                          theorem LO.Tait.close! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} (φ : F) (hp : φ Γ := by simp) (hn : φ Γ := by simp) :
                          𝓚 ⟹! Γ
                          def LO.Tait.and' {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ ψ : F} (h : φ ψ Γ) (dp : 𝓚 φ :: Γ) (dq : 𝓚 ψ :: Γ) :
                          𝓚 Γ
                          Equations
                          Instances For
                            def LO.Tait.or' {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ ψ : F} (h : φ ψ Γ) (dpq : 𝓚 φ :: ψ :: Γ) :
                            𝓚 Γ
                            Equations
                            Instances For
                              def LO.Tait.wkTail {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ : F} (d : 𝓚 Γ) :
                              𝓚 φ :: Γ
                              Equations
                              Instances For
                                def LO.Tait.rotate₁ {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ₁ φ₂ : F} (d : 𝓚 φ₂ :: φ₁ :: Γ) :
                                𝓚 φ₁ :: φ₂ :: Γ
                                Equations
                                Instances For
                                  def LO.Tait.rotate₂ {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ₁ φ₂ φ₃ : F} (d : 𝓚 φ₃ :: φ₁ :: φ₂ :: Γ) :
                                  𝓚 φ₁ :: φ₂ :: φ₃ :: Γ
                                  Equations
                                  Instances For
                                    def LO.Tait.rotate₃ {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ₁ φ₂ φ₃ φ₄ : F} (d : 𝓚 φ₄ :: φ₁ :: φ₂ :: φ₃ :: Γ) :
                                    𝓚 φ₁ :: φ₂ :: φ₃ :: φ₄ :: Γ
                                    Equations
                                    Instances For
                                      def LO.Tait.cut {F : Type u_1} {K : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : DeMorgan F} {inst✝² : Collection F K} {inst✝³ : Tait F K} [self : Cut F K] {𝓚 : K} {Δ : List F} {φ : F} :
                                      𝓚 φ :: Δ𝓚 φ :: Δ𝓚 Δ

                                      Alias of LO.Tait.Cut.cut.

                                      Equations
                                      Instances For
                                        def LO.Tait.root {F : Type u_1} {K : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : DeMorgan F} {inst✝² : Collection F K} {inst✝³ : Tait F K} [self : Axiomatized F K] {𝓚 : K} {φ : F} :
                                        φ 𝓚𝓚 ⟹. φ

                                        Alias of LO.Tait.Axiomatized.root.

                                        Equations
                                        Instances For
                                          theorem LO.Tait.cut! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {Δ : List F} {φ : F} {𝓚 : K} [Cut F K] (hp : 𝓚 ⟹! φ :: Δ) (hn : 𝓚 ⟹! φ :: Δ) :
                                          𝓚 ⟹! Δ
                                          theorem LO.Tait.root! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} [Axiomatized F K] {φ : F} (h : φ 𝓚) :
                                          𝓚 ⟹!. φ
                                          def LO.Tait.byAxm {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} [Axiomatized F K] (φ : F) (h : φ 𝓚) (hΓ : φ Γ := by simp) :
                                          𝓚 Γ
                                          Equations
                                          Instances For
                                            theorem LO.Tait.byAxm! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} [Axiomatized F K] (φ : F) (h : φ 𝓚) (hΓ : φ Γ := by simp) :
                                            𝓚 ⟹! Γ
                                            def LO.Tait.ofAxiomSubset {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 𝓛 : K} {Γ : List F} [Axiomatized F K] (h : 𝓚 𝓛) :
                                            𝓚 Γ𝓛 Γ
                                            Equations
                                            Instances For
                                              theorem LO.Tait.of_axiom_subset {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 𝓛 : K} {Γ : List F} [Axiomatized F K] (h : 𝓚 𝓛) :
                                              𝓚 ⟹! Γ𝓛 ⟹! Γ
                                              instance LO.Tait.system {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] :
                                              System F K
                                              Equations
                                              Equations
                                              theorem LO.Tait.provable_bot_iff_derivable_nil {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} [Cut F K] :
                                              𝓚 ⟹! [] 𝓚 ⊢!
                                              theorem LO.Tait.waekerThan_of_subset {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 𝓛 : K} [Axiomatized F K] (h : 𝓚 𝓛) :
                                              𝓚 ≤ₛ 𝓛
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Equations
                                              theorem LO.Tait.inconsistent_iff_provable {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} [Cut F K] :
                                              theorem LO.Tait.consistent_iff_unprovable {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} [Axiomatized F K] [Cut F K] :