@[reducible, inline]
Instances For
inductive
LO.Propositional.Classical.Derivation
{α : Type u_1}
(T : LO.Propositional.Classical.Theory α)
:
- axL: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → (Δ : List (LO.Propositional.Classical.Formula α)) → (a : α) → LO.Propositional.Classical.Derivation T (LO.Propositional.Classical.Formula.atom a :: LO.Propositional.Classical.Formula.natom a :: Δ)
- verum: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → (Δ : List (LO.Propositional.Classical.Formula α)) → LO.Propositional.Classical.Derivation T (⊤ :: Δ)
- or: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → {Δ : List (LO.Propositional.Classical.Formula α)} → {p q : LO.Propositional.Classical.Formula α} → LO.Propositional.Classical.Derivation T (p :: q :: Δ) → LO.Propositional.Classical.Derivation T (p ⋎ q :: Δ)
- and: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → {Δ : List (LO.Propositional.Classical.Formula α)} → {p q : LO.Propositional.Classical.Formula α} → LO.Propositional.Classical.Derivation T (p :: Δ) → LO.Propositional.Classical.Derivation T (q :: Δ) → LO.Propositional.Classical.Derivation T (p ⋏ q :: Δ)
- wk: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → {Δ Γ : LO.Propositional.Classical.Sequent α} → LO.Propositional.Classical.Derivation T Δ → Δ ⊆ Γ → LO.Propositional.Classical.Derivation T Γ
- cut: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → {Δ : List (LO.Propositional.Classical.Formula α)} → {p : LO.Propositional.Classical.Formula α} → LO.Propositional.Classical.Derivation T (p :: Δ) → LO.Propositional.Classical.Derivation T (∼p :: Δ) → LO.Propositional.Classical.Derivation T Δ
- root: {α : Type u_1} → {T : LO.Propositional.Classical.Theory α} → {p : LO.Propositional.Classical.Formula α} → p ∈ T → LO.Propositional.Classical.Derivation T [p]
Instances For
Equations
- LO.Propositional.Classical.instOneSidedFormulaTheory = { Derivation := LO.Propositional.Classical.Derivation }
def
LO.Propositional.Classical.Derivation.length
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{Δ : LO.Propositional.Classical.Sequent α}
:
Equations
- LO.Propositional.Classical.Derivation.length (LO.Propositional.Classical.Derivation.axL Δ a) = 0
- LO.Propositional.Classical.Derivation.length (LO.Propositional.Classical.Derivation.verum Δ) = 0
- LO.Propositional.Classical.Derivation.length d.or = (LO.Propositional.Classical.Derivation.length d).succ
- LO.Propositional.Classical.Derivation.length (dp.and dq) = (max (LO.Propositional.Classical.Derivation.length dp) (LO.Propositional.Classical.Derivation.length dq)).succ
- LO.Propositional.Classical.Derivation.length (d.wk a) = (LO.Propositional.Classical.Derivation.length d).succ
- LO.Propositional.Classical.Derivation.length (dp.cut dn) = (max (LO.Propositional.Classical.Derivation.length dp) (LO.Propositional.Classical.Derivation.length dn)).succ
- LO.Propositional.Classical.Derivation.length (LO.Propositional.Classical.Derivation.root a) = 0
Instances For
def
LO.Propositional.Classical.Derivation.cast
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{Δ : LO.Propositional.Classical.Sequent α}
{Γ : LO.Propositional.Classical.Sequent α}
(d : T ⟹ Δ)
(e : Δ = Γ)
:
T ⟹ Γ
Equations
Instances For
@[simp]
theorem
LO.Propositional.Classical.Derivation.length_cast
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{Δ : LO.Propositional.Classical.Sequent α}
{Γ : LO.Propositional.Classical.Sequent α}
(d : T ⟹ Δ)
(e : Δ = Γ)
:
def
LO.Propositional.Classical.Derivation.verum'
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{Δ : LO.Propositional.Classical.Sequent α}
(h : ⊤ ∈ Δ)
:
T ⟹ Δ
Equations
Instances For
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
def
LO.Propositional.Classical.Derivation.em
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{p : LO.Propositional.Classical.Formula α}
{Δ : LO.Propositional.Classical.Sequent α}
(hpos : p ∈ Δ)
(hneg : ∼p ∈ Δ)
:
T ⟹ Δ
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
def
LO.Propositional.Classical.Derivation.trans
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
{U : LO.Propositional.Classical.Theory α}
(F : U ⊢* T)
{Γ : LO.Propositional.Classical.Sequent α}
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
- LO.Propositional.Classical.Derivation.compact (LO.Propositional.Classical.Derivation.axL Γ_2 p) = ⟨⟨∅, ⋯⟩, LO.Propositional.Classical.Derivation.axL Γ_2 p⟩
- LO.Propositional.Classical.Derivation.compact (LO.Propositional.Classical.Derivation.verum Γ_2) = ⟨⟨∅, ⋯⟩, LO.Propositional.Classical.Derivation.verum Γ_2⟩
- LO.Propositional.Classical.Derivation.compact d.or = match LO.Propositional.Classical.Derivation.compact d with | ⟨s, d⟩ => ⟨s, LO.Propositional.Classical.Derivation.or d⟩
- LO.Propositional.Classical.Derivation.compact (d.wk ss) = match LO.Propositional.Classical.Derivation.compact d with | ⟨s, d⟩ => ⟨s, LO.Propositional.Classical.Derivation.wk d ss⟩
- LO.Propositional.Classical.Derivation.compact (LO.Propositional.Classical.Derivation.root h) = ⟨⟨{p}, ⋯⟩, LO.Propositional.Classical.Derivation.root ⋯⟩
Instances For
instance
LO.Propositional.Classical.Derivation.instCompactFormulaTheory
{α : Type u_1}
[DecidableEq α]
:
Equations
- One or more equations did not get rendered due to their size.
def
LO.Propositional.Classical.Derivation.deductionAux
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
[DecidableEq α]
{Γ : LO.Propositional.Classical.Sequent α}
{p : LO.Propositional.Classical.Formula α}
:
Equations
- One or more equations did not get rendered due to their size.
- LO.Propositional.Classical.Derivation.deductionAux (LO.Propositional.Classical.Derivation.axL Γ_2 p_1) = (LO.Propositional.Classical.Derivation.axL Γ_2 p_1).wk ⋯
- LO.Propositional.Classical.Derivation.deductionAux (LO.Propositional.Classical.Derivation.verum Γ_2) = (LO.Propositional.Classical.Derivation.verum Γ_2).wk ⋯
- LO.Propositional.Classical.Derivation.deductionAux d.or = LO.Tait.rotate₁ (LO.Tait.or (LO.Tait.wk (LO.Propositional.Classical.Derivation.deductionAux d) ⋯))
- LO.Propositional.Classical.Derivation.deductionAux (d.wk ss) = LO.Propositional.Classical.Derivation.wk (LO.Propositional.Classical.Derivation.deductionAux d) ⋯
Instances For
def
LO.Propositional.Classical.Derivation.deduction
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
[DecidableEq α]
{Γ : LO.Propositional.Classical.Sequent α}
{p : LO.Propositional.Classical.Formula α}
(d : insert p T ⟹ Γ)
:
Equations
Instances For
theorem
LO.Propositional.Classical.Derivation.inconsistent_iff_provable
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
[DecidableEq α]
{p : LO.Propositional.Classical.Formula α}
:
LO.System.Inconsistent (insert p T) ↔ T ⊢! ∼p
theorem
LO.Propositional.Classical.Derivation.consistent_iff_unprovable
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
[DecidableEq α]
{p : LO.Propositional.Classical.Formula α}
:
LO.System.Consistent (insert p T) ↔ T ⊬ ∼p
@[simp]
@[simp]
theorem
LO.Propositional.Classical.Derivation.consistent_theory_iff
{α : Type u_1}
{T : LO.Propositional.Classical.Theory α}
: