Documentation

Foundation.Propositional.Classical.Basic.Calculus

source
@[reducible, inline]
abbrev LO.Propositional.Classical.Sequent (α : Type u_2) :
Type u_2
Equations
Instances For
    source
    inductive LO.Propositional.Classical.Derivation {α : Type u_1} (T : LO.Propositional.Classical.Theory α) :
    LO.Propositional.Classical.Sequent α → Type u_1
    Instances For
      source
      instance LO.Propositional.Classical.instOneSidedFormulaTheory {α : Type u_1} :
      LO.OneSided (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Theory α)
      Equations
      • LO.Propositional.Classical.instOneSidedFormulaTheory = { Derivation := LO.Propositional.Classical.Derivation }
      source
      def LO.Propositional.Classical.Derivation.length {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ : LO.Propositional.Classical.Sequent α} :
      T ⟹ Δ → ℕ
      Equations
      Instances For
        source
        def LO.Propositional.Classical.Derivation.cast {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ Γ : LO.Propositional.Classical.Sequent α} (d : T ⟹ Δ) (e : Δ = Γ) :
        T ⟹ Γ
        Equations
        Instances For
          source
          @[simp]
          theorem LO.Propositional.Classical.Derivation.length_cast {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ Γ : LO.Propositional.Classical.Sequent α} (d : T ⟹ Δ) (e : Δ = Γ) :
          LO.Propositional.Classical.Derivation.length (LO.Propositional.Classical.Derivation.cast d e) = LO.Propositional.Classical.Derivation.length d
          source
          def LO.Propositional.Classical.Derivation.verum' {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ : LO.Propositional.Classical.Sequent α} (h : ⊤ ∈ Δ) :
          T ⟹ Δ
          Equations
          Instances For
            source
            def LO.Propositional.Classical.Derivation.axL' {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ : LO.Propositional.Classical.Sequent α} (a : α) (h : LO.Propositional.Classical.Formula.atom a ∈ Δ) (hn : LO.Propositional.Classical.Formula.natom a ∈ Δ) :
            T ⟹ Δ
            Equations
            Instances For
              source
              def LO.Propositional.Classical.Derivation.em {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {φ : LO.Propositional.Classical.Formula α} {Δ : LO.Propositional.Classical.Sequent α} (hpos : φ ∈ Δ) (hneg : ∼φ ∈ Δ) :
              T ⟹ Δ
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance LO.Propositional.Classical.Derivation.instTaitFormulaTheory {α : Type u_1} :
                LO.Tait (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Theory α)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                instance LO.Propositional.Classical.Derivation.instCutFormulaTheory {α : Type u_1} :
                LO.Tait.Cut (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Theory α)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                def LO.Propositional.Classical.Derivation.trans {α : Type u_1} {T U : LO.Propositional.Classical.Theory α} (F : U ⊢* T) {Γ : LO.Propositional.Classical.Sequent α} :
                T ⟹ Γ → U ⟹ Γ
                Equations
                Instances For
                  source
                  instance LO.Propositional.Classical.Derivation.instAxiomatizedFormulaTheory {α : Type u_1} :
                  LO.Tait.Axiomatized (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Theory α)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def LO.Propositional.Classical.Derivation.compact {α : Type u_1} {T : LO.Propositional.Classical.Theory α} [DecidableEq α] {Γ : LO.Propositional.Classical.Sequent α} :
                  T ⟹ Γ → (s : { s : Finset (LO.Propositional.Classical.Formula α) // ↑s ⊆ T }) × ↑↑s ⟹ Γ
                  Equations
                  Instances For
                    source
                    instance LO.Propositional.Classical.Derivation.instCompactFormulaTheory {α : Type u_1} [DecidableEq α] :
                    LO.System.Compact (LO.Propositional.Classical.Theory α)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    def LO.Propositional.Classical.Derivation.deductionAux {α : Type u_1} {T : LO.Propositional.Classical.Theory α} [DecidableEq α] {Γ : LO.Propositional.Classical.Sequent α} {φ : LO.Propositional.Classical.Formula α} :
                    T ⟹ Γ → T \ {φ} ⟹ ∼φ :: Γ
                    Equations
                    Instances For
                      source
                      def LO.Propositional.Classical.Derivation.deduction {α : Type u_1} {T : LO.Propositional.Classical.Theory α} [DecidableEq α] {Γ : LO.Propositional.Classical.Sequent α} {φ : LO.Propositional.Classical.Formula α} (d : insert φ T ⟹ Γ) :
                      T ⟹ ∼φ :: Γ
                      Equations
                      Instances For
                        source
                        theorem LO.Propositional.Classical.Derivation.inconsistent_iff_provable {α : Type u_1} {T : LO.Propositional.Classical.Theory α} [DecidableEq α] {φ : LO.Propositional.Classical.Formula α} :
                        LO.System.Inconsistent (insert φ T) ↔ T ⊢! ∼φ
                        source
                        theorem LO.Propositional.Classical.Derivation.consistent_iff_unprovable {α : Type u_1} {T : LO.Propositional.Classical.Theory α} [DecidableEq α] {φ : LO.Propositional.Classical.Formula α} :
                        LO.System.Consistent (insert φ T) ↔ T ⊬ ∼φ
                        source
                        @[simp]
                        theorem LO.Propositional.Classical.Derivation.inconsistent_theory_iff {α : Type u_1} {T : LO.Propositional.Classical.Theory α} :
                        LO.System.Inconsistent (LO.System.theory T) ↔ LO.System.Inconsistent T
                        source
                        @[simp]
                        theorem LO.Propositional.Classical.Derivation.consistent_theory_iff {α : Type u_1} {T : LO.Propositional.Classical.Theory α} :
                        LO.System.Consistent (LO.System.theory T) ↔ LO.System.Consistent T