ProvabilityLogic.Gentzen.A.Basic

source

inductive LogicA.ProofGentzen {α : Type u} [DecidableEq α] :

TwoLayeredSequent α → Type u

axm {α : Type u} [DecidableEq α] (l : Fin 2) (A : Formula α) : ProofGentzen ({A} ⟹[l] {A})
botL {α : Type u} [DecidableEq α] (l : Fin 2) : ProofGentzen ({⊥} ⟹[l] ∅)
wkL {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Γ' Δ : FormulaFinset α} : ProofGentzen (Γ ⟹[l] Δ) → autoParam (Γ ⊆ Γ') _auto_1 → ProofGentzen (Γ' ⟹[l] Δ)
wkR {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ Δ' : FormulaFinset α} : ProofGentzen (Γ ⟹[l] Δ) → autoParam (Δ ⊆ Δ') _auto_3 → ProofGentzen (Γ ⟹[l] Δ')
impL {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} : ProofGentzen (Γ ⟹[l] insert A Δ) → ProofGentzen (insert B Γ ⟹[l] Δ) → ProofGentzen (insert (A 🡒 B) Γ ⟹[l] Δ)
impR {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} : ProofGentzen (insert A Γ ⟹[l] insert B Δ) → ProofGentzen (Γ ⟹[l] insert (A 🡒 B) Δ)
liftUp {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : ProofGentzen (Γ ⟹[0] Δ) → ProofGentzen (Γ ⟹[1] Δ)
boxGL {α : Type u} [DecidableEq α] {Γ : FormulaFinset α} {A : Formula α} : ProofGentzen (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A}) → ProofGentzen (Γ.box ⟹[0] {□A})
boxGP {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {n : ℕ} : ProofGentzen (Γ ⟹[1] insert (□^[n]⊥) Δ) → ProofGentzen (Γ ⟹[1] Δ)

Instances For

source

def LogicA.«term⊢ᵍ[A]!_» :

Lean.ParserDescr

Equations

LogicA.«term⊢ᵍ[A]!_» = Lean.ParserDescr.node `LogicA.«term⊢ᵍ[A]!_» 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵍ[A]! ") (Lean.ParserDescr.cat `term 120))

Instances For

source

@[reducible, inline]

abbrev LogicA.ProvableGentzen {α : Type u} [DecidableEq α] (S : TwoLayeredSequent α) :

Prop

Equations

LogicA.ProvableGentzen S = Nonempty (LogicA.ProofGentzen S)

Instances For

source

def LogicA.«term⊢ᵍ[A]_» :

Lean.ParserDescr

Equations

LogicA.«term⊢ᵍ[A]_» = Lean.ParserDescr.node `LogicA.«term⊢ᵍ[A]_» 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵍ[A] ") (Lean.ParserDescr.cat `term 120))

Instances For

source

@[irreducible]

def LogicA.ofProofGentzen {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} :

⊢ᵍ[GL]! (Γ ⟹ Δ) → ProofGentzen (Γ ⟹[0] Δ)

Equations

LogicA.ofProofGentzen (LogicGL.ProofGentzen.axm A) = LogicA.ProofGentzen.axm 0 A
LogicA.ofProofGentzen LogicGL.ProofGentzen.botL = LogicA.ProofGentzen.botL 0
LogicA.ofProofGentzen (h.wkL h') = (LogicA.ofProofGentzen h).wkL h'
LogicA.ofProofGentzen (h.wkR h') = (LogicA.ofProofGentzen h).wkR h'
LogicA.ofProofGentzen (h₁.impL h₂) = (LogicA.ofProofGentzen h₁).impL (LogicA.ofProofGentzen h₂)
LogicA.ofProofGentzen h.impR = (LogicA.ofProofGentzen h).impR
LogicA.ofProofGentzen h.boxGL = (LogicA.ofProofGentzen h).boxGL

Instances For

source

@[irreducible]

def LogicA.toProofGentzen {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} :

ProofGentzen (Γ ⟹[0] Δ) → ⊢ᵍ[GL]! (Γ ⟹ Δ)

Equations

LogicA.toProofGentzen (LogicA.ProofGentzen.axm 0 A) = LogicGL.ProofGentzen.axm A
LogicA.toProofGentzen (LogicA.ProofGentzen.botL 0) = LogicGL.ProofGentzen.botL
LogicA.toProofGentzen (h.wkL h') = (LogicA.toProofGentzen h).wkL h'
LogicA.toProofGentzen (h.wkR h') = (LogicA.toProofGentzen h).wkR h'
LogicA.toProofGentzen (h₁.impL h₂) = (LogicA.toProofGentzen h₁).impL (LogicA.toProofGentzen h₂)
LogicA.toProofGentzen h.impR = (LogicA.toProofGentzen h).impR
LogicA.toProofGentzen h.boxGL = (LogicA.toProofGentzen h).boxGL

Instances For

source

theorem LogicA.iff_provableGentzen_provable_zero {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} :

⊢ᵍ[GL] (Γ ⟹ Δ) ↔ ProvableGentzen (Γ ⟹[0] Δ)

source

theorem LogicA.ProvableGentzen.axm {α : Type u} [DecidableEq α] (l : Fin 2) (A : Formula α) :

ProvableGentzen ({A} ⟹[l] {A})

source

theorem LogicA.ProvableGentzen.botL {α : Type u} [DecidableEq α] (l : Fin 2) :

ProvableGentzen ({⊥} ⟹[l] ∅)

source

theorem LogicA.ProvableGentzen.wkL {α : Type u} [DecidableEq α] {Γ Γ' Δ : FormulaFinset α} {l : Fin 2} (h : ProvableGentzen (Γ ⟹[l] Δ)) (hΓ : Γ ⊆ Γ') :

ProvableGentzen (Γ' ⟹[l] Δ)

source

theorem LogicA.ProvableGentzen.wkR {α : Type u} [DecidableEq α] {Γ Δ Δ' : FormulaFinset α} {l : Fin 2} (h : ProvableGentzen (Γ ⟹[l] Δ)) (hΔ : Δ ⊆ Δ') :

ProvableGentzen (Γ ⟹[l] Δ')

source

theorem LogicA.ProvableGentzen.impL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {A B : Formula α} {l : Fin 2} (h₁ : ProvableGentzen (Γ ⟹[l] insert A Δ)) (h₂ : ProvableGentzen (insert B Γ ⟹[l] Δ)) :

ProvableGentzen (insert (A 🡒 B) Γ ⟹[l] Δ)

source

theorem LogicA.ProvableGentzen.impR {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {A B : Formula α} {l : Fin 2} (h : ProvableGentzen (insert A Γ ⟹[l] insert B Δ)) :

ProvableGentzen (Γ ⟹[l] insert (A 🡒 B) Δ)

source

theorem LogicA.ProvableGentzen.liftUp {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (h : ProvableGentzen (Γ ⟹[0] Δ)) :

ProvableGentzen (Γ ⟹[1] Δ)

source

theorem LogicA.ProvableGentzen.boxGL {α : Type u} [DecidableEq α] {Γ : FormulaFinset α} {A : Formula α} (h : ProvableGentzen (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A})) :

ProvableGentzen (Γ.box ⟹[0] {□A})

source

theorem LogicA.ProvableGentzen.boxGP {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {n : ℕ} :

ProvableGentzen (Γ ⟹[1] insert (□^[n]⊥) Δ) → ProvableGentzen (Γ ⟹[1] Δ)

source

theorem LogicA.ProvableGentzen.rec {α : Type u} [DecidableEq α] {motive : (S : TwoLayeredSequent α) → ProvableGentzen S → Prop} (axm : ∀ (l : Fin 2) (A : Formula α), motive ({A} ⟹[l] {A}) ⋯) (botL : ∀ (l : Fin 2), motive ({⊥} ⟹[l] ∅) ⋯) (wkL : ∀ {l : Fin 2} {Γ Γ' Δ : FormulaFinset α} (h : ProvableGentzen (Γ ⟹[l] Δ)) (hΓ : Γ ⊆ Γ'), motive (Γ ⟹[l] Δ) h → motive (Γ' ⟹[l] Δ) ⋯) (wkR : ∀ {l : Fin 2} {Γ Δ Δ' : FormulaFinset α} (h : ProvableGentzen (Γ ⟹[l] Δ)) (hΔ : Δ ⊆ Δ'), motive (Γ ⟹[l] Δ) h → motive (Γ ⟹[l] Δ') ⋯) (impL : ∀ {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} (h₁ : ProvableGentzen (Γ ⟹[l] insert A Δ)) (h₂ : ProvableGentzen (insert B Γ ⟹[l] Δ)), motive (Γ ⟹[l] insert A Δ) h₁ → motive (insert B Γ ⟹[l] Δ) h₂ → motive (insert (A 🡒 B) Γ ⟹[l] Δ) ⋯) (impR : ∀ {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} (h : ProvableGentzen (insert A Γ ⟹[l] insert B Δ)), motive (insert A Γ ⟹[l] insert B Δ) h → motive (Γ ⟹[l] insert (A 🡒 B) Δ) ⋯) (liftUp : ∀ {Γ Δ : FormulaFinset α} (h : ProvableGentzen (Γ ⟹[0] Δ)), motive (Γ ⟹[0] Δ) h → motive (Γ ⟹[1] Δ) ⋯) (boxGL : ∀ {Γ : FormulaFinset α} {A : Formula α} (h : ProvableGentzen (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A})), motive (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A}) h → motive (Γ.box ⟹[0] {□A}) ⋯) (boxGP : ∀ {Γ Δ : FormulaFinset α} {n : ℕ} (h : ProvableGentzen (Γ ⟹[1] insert (□^[n]⊥) Δ)), motive (Γ ⟹[1] insert (□^[n]⊥) Δ) h → motive (Γ ⟹[1] Δ) ⋯) {S : TwoLayeredSequent α} (h : ProvableGentzen S) :

motive S h

source

def LogicA.ProvableGentzen.«term⊬ᵍ[A]_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LogicA.ProvableGentzen.iff_unprovableGentzen_isEmpty_ProofGentzen {α : Type u} [DecidableEq α] {S : TwoLayeredSequent α} :

(fun (x : TwoLayeredSequent α) => ¬ProvableGentzen x) S ↔ IsEmpty (ProofGentzen S)

source

theorem LogicA.ProvableGentzen.union {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (l : Fin 2) (A : Formula α) (hΓ : A ∈ Γ := by grind) (hΔ : A ∈ Δ := by grind) :

ProvableGentzen (Γ ⟹[l] Δ)

source

theorem LogicA.ProvableGentzen.union' {α : Type u} [DecidableEq α] (l : Fin 2) (A : Formula α) {S : Sequent α} (hΓ : A ∈ S.ant := by grind) (hΔ : A ∈ S.suc := by grind) :

ProvableGentzen (S.ant ⟹[l] S.suc)

source

theorem LogicA.ProvableGentzen.botL_mem {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (l : Fin 2) (h : ⊥ ∈ Γ := by grind) :

ProvableGentzen (Γ ⟹[l] Δ)

source

theorem LogicA.ProvableGentzen.not_provable_zero_of_not_provable_one {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} :

(fun (x : TwoLayeredSequent α) => ¬ProvableGentzen x) (Γ ⟹[1] Δ) → (fun (x : TwoLayeredSequent α) => ¬ProvableGentzen x) (Γ ⟹[0] Δ)

source

theorem LogicA.ProvableGentzen.of_provableGentzen_insert_boxItr_bot {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {n : ℕ} (h : ⊢ᵍ[GL] (Γ ⟹ insert (□^[n]⊥) Δ)) :

ProvableGentzen (Γ ⟹[1] Δ)

source

theorem LogicA.not_provableGentzen_of_not_provable_one {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (h : ¬ProvableGentzen (Γ ⟹[1] Δ)) :

¬⊢ᵍ[GL] (Γ ⟹ Δ)

source

inductive LogicA.GentzenWithCutProof {α : Type u} [DecidableEq α] :

TwoLayeredSequent α → Type u

axm {α : Type u} [DecidableEq α] (l : Fin 2) (A : Formula α) : GentzenWithCutProof ({A} ⟹[l] {A})
botL {α : Type u} [DecidableEq α] (l : Fin 2) : GentzenWithCutProof ({⊥} ⟹[l] ∅)
wkL {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Γ' Δ : FormulaFinset α} : GentzenWithCutProof (Γ ⟹[l] Δ) → autoParam (Γ ⊆ Γ') _auto_1 → GentzenWithCutProof (Γ' ⟹[l] Δ)
wkR {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ Δ' : FormulaFinset α} : GentzenWithCutProof (Γ ⟹[l] Δ) → autoParam (Δ ⊆ Δ') _auto_3 → GentzenWithCutProof (Γ ⟹[l] Δ')
impL {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} : GentzenWithCutProof (Γ ⟹[l] insert A Δ) → GentzenWithCutProof (insert B Γ ⟹[l] Δ) → GentzenWithCutProof (insert (A 🡒 B) Γ ⟹[l] Δ)
impR {α : Type u} [DecidableEq α] {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} : GentzenWithCutProof (insert A Γ ⟹[l] insert B Δ) → GentzenWithCutProof (Γ ⟹[l] insert (A 🡒 B) Δ)
liftUp {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : GentzenWithCutProof (Γ ⟹[0] Δ) → GentzenWithCutProof (Γ ⟹[1] Δ)
boxGL {α : Type u} [DecidableEq α] {Γ : FormulaFinset α} {A : Formula α} : GentzenWithCutProof (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A}) → GentzenWithCutProof (Γ.box ⟹[0] {□A})
boxGP {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {n : ℕ} : GentzenWithCutProof (Γ ⟹[1] insert (□^[n]⊥) Δ) → GentzenWithCutProof (Γ ⟹[1] Δ)
cut {α : Type u} [DecidableEq α] {l : Fin 2} {Γ₁ Γ₂ Δ₁ Δ₂ : FormulaFinset α} {A : Formula α} : GentzenWithCutProof (Γ₁ ⟹[l] insert A Δ₁) → GentzenWithCutProof (insert A Γ₂ ⟹[l] Δ₂) → GentzenWithCutProof (Γ₁ ∪ Γ₂ ⟹[l] Δ₁ ∪ Δ₂)

Instances For

source

def LogicA.«term⊢ᵍᶜ[A]!_» :

Lean.ParserDescr

Equations

LogicA.«term⊢ᵍᶜ[A]!_» = Lean.ParserDescr.node `LogicA.«term⊢ᵍᶜ[A]!_» 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵍᶜ[A]! ") (Lean.ParserDescr.cat `term 120))

Instances For

source

@[reducible, inline]

abbrev LogicA.GentzenWithCutProvable {α : Type u} [DecidableEq α] (S : TwoLayeredSequent α) :

Prop

Equations

LogicA.GentzenWithCutProvable S = Nonempty (LogicA.GentzenWithCutProof S)

Instances For

source

def LogicA.«term⊢ᵍᶜ[A]_» :

Lean.ParserDescr

Equations

LogicA.«term⊢ᵍᶜ[A]_» = Lean.ParserDescr.node `LogicA.«term⊢ᵍᶜ[A]_» 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵍᶜ[A] ") (Lean.ParserDescr.cat `term 120))

Instances For

source

def LogicA.GentzenWithCutProof.ofProofGentzen {α : Type u} [DecidableEq α] {S : TwoLayeredSequent α} :

ProofGentzen S → GentzenWithCutProof S

Equations

Instances For

source

@[irreducible]

def LogicA.GentzenWithCutProof.toGentzenWithCutProofGL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} :

GentzenWithCutProof (Γ ⟹[0] Δ) → ⊢ᵍᶜ[GL]! (Γ ⟹ Δ)

Equations

Instances For

source

theorem LogicA.GentzenWithCutProvable.of_without_cut {α : Type u} [DecidableEq α] {S : TwoLayeredSequent α} :

ProvableGentzen S → GentzenWithCutProvable S

source

theorem LogicA.GentzenWithCutProvable.toGentzenWithCutProvableGL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[0] Δ)) :

⊢ᵍᶜ[GL] (Γ ⟹ Δ)

source

theorem LogicA.GentzenWithCutProvable.toProvableGentzenGL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[0] Δ)) :

⊢ᵍ[GL] (Γ ⟹ Δ)

source

theorem LogicA.GentzenWithCutProvable.axm {α : Type u} [DecidableEq α] (l : Fin 2) (A : Formula α) :

GentzenWithCutProvable ({A} ⟹[l] {A})

source

theorem LogicA.GentzenWithCutProvable.botL {α : Type u} [DecidableEq α] (l : Fin 2) :

GentzenWithCutProvable ({⊥} ⟹[l] ∅)

source

theorem LogicA.GentzenWithCutProvable.wkL {α : Type u} [DecidableEq α] {Γ Γ' Δ : FormulaFinset α} {l : Fin 2} (h : GentzenWithCutProvable (Γ ⟹[l] Δ)) (h' : Γ ⊆ Γ') :

GentzenWithCutProvable (Γ' ⟹[l] Δ)

source

theorem LogicA.GentzenWithCutProvable.wkR {α : Type u} [DecidableEq α] {Γ Δ Δ' : FormulaFinset α} {l : Fin 2} (h : GentzenWithCutProvable (Γ ⟹[l] Δ)) (h' : Δ ⊆ Δ') :

GentzenWithCutProvable (Γ ⟹[l] Δ')

source

theorem LogicA.GentzenWithCutProvable.impL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {A B : Formula α} {l : Fin 2} (h₁ : GentzenWithCutProvable (Γ ⟹[l] insert A Δ)) (h₂ : GentzenWithCutProvable (insert B Γ ⟹[l] Δ)) :

GentzenWithCutProvable (insert (A 🡒 B) Γ ⟹[l] Δ)

source

theorem LogicA.GentzenWithCutProvable.impR {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {A B : Formula α} {l : Fin 2} (h : GentzenWithCutProvable (insert A Γ ⟹[l] insert B Δ)) :

GentzenWithCutProvable (Γ ⟹[l] insert (A 🡒 B) Δ)

source

theorem LogicA.GentzenWithCutProvable.liftUp {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[0] Δ)) :

GentzenWithCutProvable (Γ ⟹[1] Δ)

source

theorem LogicA.GentzenWithCutProvable.boxGL {α : Type u} [DecidableEq α] {Γ : FormulaFinset α} {A : Formula α} (h : GentzenWithCutProvable (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A})) :

GentzenWithCutProvable (Γ.box ⟹[0] {□A})

source

theorem LogicA.GentzenWithCutProvable.boxGP {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} {n : ℕ} (h : GentzenWithCutProvable (Γ ⟹[1] insert (□^[n]⊥) Δ)) :

GentzenWithCutProvable (Γ ⟹[1] Δ)

source

theorem LogicA.GentzenWithCutProvable.cut {α : Type u} [DecidableEq α] {Γ₁ Γ₂ Δ₁ Δ₂ : FormulaFinset α} {A : Formula α} {l : Fin 2} (h₁ : GentzenWithCutProvable (Γ₁ ⟹[l] insert A Δ₁)) (h₂ : GentzenWithCutProvable (insert A Γ₂ ⟹[l] Δ₂)) :

GentzenWithCutProvable (Γ₁ ∪ Γ₂ ⟹[l] Δ₁ ∪ Δ₂)

source

theorem LogicA.GentzenWithCutProvable.rec {α : Type u} [DecidableEq α] {motive : (S : TwoLayeredSequent α) → GentzenWithCutProvable S → Prop} (axm : ∀ (l : Fin 2) (A : Formula α), motive ({A} ⟹[l] {A}) ⋯) (botL : ∀ (l : Fin 2), motive ({⊥} ⟹[l] ∅) ⋯) (wkL : ∀ {l : Fin 2} {Γ Γ' Δ : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[l] Δ)) (h' : Γ ⊆ Γ'), motive (Γ ⟹[l] Δ) h → motive (Γ' ⟹[l] Δ) ⋯) (wkR : ∀ {l : Fin 2} {Γ Δ Δ' : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[l] Δ)) (h' : Δ ⊆ Δ'), motive (Γ ⟹[l] Δ) h → motive (Γ ⟹[l] Δ') ⋯) (impL : ∀ {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} (h₁ : GentzenWithCutProvable (Γ ⟹[l] insert A Δ)) (h₂ : GentzenWithCutProvable (insert B Γ ⟹[l] Δ)), motive (Γ ⟹[l] insert A Δ) h₁ → motive (insert B Γ ⟹[l] Δ) h₂ → motive (insert (A 🡒 B) Γ ⟹[l] Δ) ⋯) (impR : ∀ {l : Fin 2} {Γ Δ : FormulaFinset α} {A B : Formula α} (h : GentzenWithCutProvable (insert A Γ ⟹[l] insert B Δ)), motive (insert A Γ ⟹[l] insert B Δ) h → motive (Γ ⟹[l] insert (A 🡒 B) Δ) ⋯) (liftUp : ∀ {Γ Δ : FormulaFinset α} (h : GentzenWithCutProvable (Γ ⟹[0] Δ)), motive (Γ ⟹[0] Δ) h → motive (Γ ⟹[1] Δ) ⋯) (boxGL : ∀ {Γ : FormulaFinset α} {A : Formula α} (h : GentzenWithCutProvable (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A})), motive (insert (□A) (Γ ∪ Γ.box) ⟹[0] {A}) h → motive (Γ.box ⟹[0] {□A}) ⋯) (boxGP : ∀ {Γ Δ : FormulaFinset α} {n : ℕ} (h : GentzenWithCutProvable (Γ ⟹[1] insert (□^[n]⊥) Δ)), motive (Γ ⟹[1] insert (□^[n]⊥) Δ) h → motive (Γ ⟹[1] Δ) ⋯) (cut : ∀ {l : Fin 2} {Γ₁ Γ₂ Δ₁ Δ₂ : FormulaFinset α} {A : Formula α} (h₁ : GentzenWithCutProvable (Γ₁ ⟹[l] insert A Δ₁)) (h₂ : GentzenWithCutProvable (insert A Γ₂ ⟹[l] Δ₂)), motive (Γ₁ ⟹[l] insert A Δ₁) h₁ → motive (insert A Γ₂ ⟹[l] Δ₂) h₂ → motive (Γ₁ ∪ Γ₂ ⟹[l] Δ₁ ∪ Δ₂) ⋯) {S : TwoLayeredSequent α} (h : GentzenWithCutProvable S) :

motive S h

source

theorem LogicA.GentzenWithCutProvable.neg_boxItr_bot {α : Type u} [DecidableEq α] (n : ℕ) :

GentzenWithCutProvable (∅ ⟹[1] {∼□^[n]⊥})

source

theorem LogicA.GentzenWithCutProvable.mdp {α : Type u} [DecidableEq α] {A B : Formula α} (hAB : GentzenWithCutProvable (∅ ⟹[1] {A 🡒 B})) (hA : GentzenWithCutProvable (∅ ⟹[1] {A})) :

GentzenWithCutProvable (∅ ⟹[1] {B})