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] Δ)

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))

@[reducible, inline]

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

Equations

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

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))

@[irreducible]

def LogicA.ofProofGentzen {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : ⊢ᵍ[GL]! (Γ ⟹ Δ) → ProofGentzen (Γ ⟹[0] Δ)

Embed a level-0 LogicGL proof into level-0 LogicA.

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

@[irreducible]

def LogicA.toProofGentzen {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : ProofGentzen (Γ ⟹[0] Δ) → ⊢ᵍ[GL]! (Γ ⟹ Δ)

Extract a level-0 LogicGL proof from level-0 LogicA.

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

theorem LogicA.iff_provableGentzen_provable_zero {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : ⊢ᵍ[GL] (Γ ⟹ Δ) ↔ ProvableGentzen (Γ ⟹[0] Δ)

Level-0 LogicA.ProvableGentzen-provability is exactly (plain, cut-free) GL-provability.

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

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

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

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

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] Δ)

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) Δ)

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

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

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

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

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

Equations

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

theorem LogicA.ProvableGentzen.iff_unprovableGentzen_isEmpty_ProofGentzen {α : Type u} [DecidableEq α] {S : TwoLayeredSequent α} : (fun (x : TwoLayeredSequent α) => ¬ProvableGentzen x) S ↔ IsEmpty (ProofGentzen S)

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

Initial sequents with side formulas, at any level.

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)

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

botL with side formulas, at any level.

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] Δ)

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

Embed a cut-free LogicGL proof of Γ ⟹ insert (□^[n]⊥) Δ into level-1 cut-free LogicA provability of Γ ⟹[1] Δ.

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

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] Δ₁ ∪ Δ₂)

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))

@[reducible, inline]

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

Equations

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

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))

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

Equations

• LogicA.GentzenWithCutProof.ofProofGentzen (LogicA.ProofGentzen.axm l A) = LogicA.GentzenWithCutProof.axm l A
• LogicA.GentzenWithCutProof.ofProofGentzen (LogicA.ProofGentzen.botL l) = LogicA.GentzenWithCutProof.botL l
• LogicA.GentzenWithCutProof.ofProofGentzen (h.wkL h') = (LogicA.GentzenWithCutProof.ofProofGentzen h).wkL h'
• LogicA.GentzenWithCutProof.ofProofGentzen (h.wkR h') = (LogicA.GentzenWithCutProof.ofProofGentzen h).wkR h'
• LogicA.GentzenWithCutProof.ofProofGentzen (h₁.impL h₂) = (LogicA.GentzenWithCutProof.ofProofGentzen h₁).impL (LogicA.GentzenWithCutProof.ofProofGentzen h₂)
• LogicA.GentzenWithCutProof.ofProofGentzen h.impR = (LogicA.GentzenWithCutProof.ofProofGentzen h).impR
• LogicA.GentzenWithCutProof.ofProofGentzen h.liftUp = (LogicA.GentzenWithCutProof.ofProofGentzen h).liftUp
• LogicA.GentzenWithCutProof.ofProofGentzen h.boxGL = (LogicA.GentzenWithCutProof.ofProofGentzen h).boxGL
• LogicA.GentzenWithCutProof.ofProofGentzen h.boxGP = (LogicA.GentzenWithCutProof.ofProofGentzen h).boxGP

@[irreducible]

def LogicA.GentzenWithCutProof.toGentzenWithCutProofGL {α : Type u} [DecidableEq α] {Γ Δ : FormulaFinset α} : GentzenWithCutProof (Γ ⟹[0] Δ) → ⊢ᵍᶜ[GL]! (Γ ⟹ Δ)

Equations

• (LogicA.GentzenWithCutProof.axm 0 A).toGentzenWithCutProofGL = LogicGL.GentzenWithCutProof.axm A
• (LogicA.GentzenWithCutProof.botL 0).toGentzenWithCutProofGL = LogicGL.GentzenWithCutProof.botL
• (h.wkL h').toGentzenWithCutProofGL = h.toGentzenWithCutProofGL.wkL h'
• (h.wkR h').toGentzenWithCutProofGL = h.toGentzenWithCutProofGL.wkR h'
• (h₁.impL h₂).toGentzenWithCutProofGL = h₁.toGentzenWithCutProofGL.impL h₂.toGentzenWithCutProofGL
• h.impR.toGentzenWithCutProofGL = h.toGentzenWithCutProofGL.impR
• h.boxGL.toGentzenWithCutProofGL = h.toGentzenWithCutProofGL.boxGL
• (h₁.cut h₂).toGentzenWithCutProofGL = h₁.toGentzenWithCutProofGL.cut h₂.toGentzenWithCutProofGL

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

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

Prop-level version of LogicA.GentzenWithCutProof.toGentzenWithCutProofGL.

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

Level-0 LogicA-with-cut provability implies cut-free LogicGL-Gentzen provability.

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

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

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

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

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] Δ)

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) Δ)

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

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

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

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] Δ₁ ∪ Δ₂)

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

theorem LogicA.GentzenWithCutProvable.neg_boxItr_bot {α : Type u} [DecidableEq α] (n : ℕ) : GentzenWithCutProvable (∅ ⟹[1] {∼□^[n]⊥})

The axiom ∼□^[n]⊥ is with-cut-provable at level 1.

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

Modus ponens for level-1 with-cut provability, via the cut rule.