Documentation

Foundation.Propositional.Classical.Basic.Calculus

source
@[reducible, inline]
abbrev LO.Propositional.Classical.Sequent (α : Type u_2) :
Type u_2
Equations
source
inductive LO.Propositional.Classical.Derivation {α : Type u_1} (T : Theory α) :
Sequent α → Type u_1
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
source
def LO.Propositional.Classical.Derivation.cast {α : Type u_1} {T : Theory α} {Δ Γ : Sequent α} (d : T ⟹ Δ) (e : Δ = Γ) :
T ⟹ Γ
Equations
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
source
def LO.Propositional.Classical.Derivation.axL' {α : Type u_1} {T : Theory α} {Δ : Sequent α} (a : α) (h : Formula.atom a ∈ Δ) (hn : Formula.natom a ∈ Δ) :
T ⟹ Δ
Equations
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.
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
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
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
source
def LO.Propositional.Classical.Derivation.deduction {α : Type u_1} {T : Theory α} [DecidableEq α] {Γ : Sequent α} {φ : Formula α} (d : insert φ T ⟹ Γ) :
T ⟹ ∼φ :: Γ
Equations
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