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