Defining GL-ext proof systems.

Here we define the GL-ext proof system along with finitization and basic properties. We use the namespace SplitCut to distinguish from our general GL-proofs.

Basic components of the GL-ext proof system.

inductive SplitCut.RuleApp : Type

Rule applications for the GL-ext proof system.

• skp (Δ : SplitSequent) : RuleApp
• cutₗ (Δ : SplitSequent) (A : Formula) : RuleApp
• cutᵣ (Δ : SplitSequent) (A : Formula) : RuleApp
• wkₗ (Δ : SplitSequent) (A : Formula) : Sum.inl A ∈ Δ → RuleApp
• wkᵣ (Δ : SplitSequent) (A : Formula) : Sum.inr A ∈ Δ → RuleApp
• topₗ (Δ : SplitSequent) : Sum.inl ⊤ ∈ Δ → RuleApp
• topᵣ (Δ : SplitSequent) : Sum.inr ⊤ ∈ Δ → RuleApp
• axₗₗ (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp
• axₗᵣ (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp
• axᵣₗ (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp
• axᵣᵣ (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp
• andₗ (Δ : SplitSequent) (A B : Formula) : Sum.inl (A&B) ∈ Δ → RuleApp
• andᵣ (Δ : SplitSequent) (A B : Formula) : Sum.inr (A&B) ∈ Δ → RuleApp
• orₗ (Δ : SplitSequent) (A B : Formula) : Sum.inl (A v B) ∈ Δ → RuleApp
• orᵣ (Δ : SplitSequent) (A B : Formula) : Sum.inr (A v B) ∈ Δ → RuleApp
• boxₗ (Δ : SplitSequent) (A : Formula) : Sum.inl (□A) ∈ Δ → RuleApp
• boxᵣ (Δ : SplitSequent) (A : Formula) : Sum.inr (□A) ∈ Δ → RuleApp

def SplitCut.T : CategoryTheory.Functor Type Type

Endofunctor for the GL-ext proof system.

Equations

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

def SplitCut.fₚ : RuleApp → SplitSequent

Given a RuleApp, obtain the principal formulas.

Equations

• SplitCut.fₚ (SplitCut.RuleApp.skp Δ) = ∅
• SplitCut.fₚ (SplitCut.RuleApp.cutₗ Δ A) = ∅
• SplitCut.fₚ (SplitCut.RuleApp.cutᵣ Δ A) = ∅
• SplitCut.fₚ (SplitCut.RuleApp.wkₗ Δ A a) = {Sum.inl A}
• SplitCut.fₚ (SplitCut.RuleApp.wkᵣ Δ A a) = {Sum.inr A}
• SplitCut.fₚ (SplitCut.RuleApp.topₗ Δ a) = {Sum.inl ⊤}
• SplitCut.fₚ (SplitCut.RuleApp.topᵣ Δ a) = {Sum.inr ⊤}
• SplitCut.fₚ (SplitCut.RuleApp.axₗₗ Δ n a) = {Sum.inl (at n), Sum.inl (na n)}
• SplitCut.fₚ (SplitCut.RuleApp.axₗᵣ Δ n a) = {Sum.inl (at n), Sum.inr (na n)}
• SplitCut.fₚ (SplitCut.RuleApp.axᵣₗ Δ n a) = {Sum.inr (at n), Sum.inl (na n)}
• SplitCut.fₚ (SplitCut.RuleApp.axᵣᵣ Δ n a) = {Sum.inr (at n), Sum.inr (na n)}
• SplitCut.fₚ (SplitCut.RuleApp.andₗ Δ A B a) = {Sum.inl (A&B)}
• SplitCut.fₚ (SplitCut.RuleApp.andᵣ Δ A B a) = {Sum.inr (A&B)}
• SplitCut.fₚ (SplitCut.RuleApp.orₗ Δ A B a) = {Sum.inl (A v B)}
• SplitCut.fₚ (SplitCut.RuleApp.orᵣ Δ A B a) = {Sum.inr (A v B)}
• SplitCut.fₚ (SplitCut.RuleApp.boxₗ Δ A a) = {Sum.inl (□A)}
• SplitCut.fₚ (SplitCut.RuleApp.boxᵣ Δ A a) = {Sum.inr (□A)}

def SplitCut.f : RuleApp → SplitSequent

Given a RuleApp, obtain the split sequent.

Equations

• SplitCut.f (SplitCut.RuleApp.skp Δ) = Δ
• SplitCut.f (SplitCut.RuleApp.cutₗ Δ A) = Δ
• SplitCut.f (SplitCut.RuleApp.cutᵣ Δ A) = Δ
• SplitCut.f (SplitCut.RuleApp.wkₗ Δ A a) = Δ
• SplitCut.f (SplitCut.RuleApp.wkᵣ Δ A a) = Δ
• SplitCut.f (SplitCut.RuleApp.topₗ Δ a) = Δ
• SplitCut.f (SplitCut.RuleApp.topᵣ Δ a) = Δ
• SplitCut.f (SplitCut.RuleApp.axₗₗ Δ n a) = Δ
• SplitCut.f (SplitCut.RuleApp.axₗᵣ Δ n a) = Δ
• SplitCut.f (SplitCut.RuleApp.axᵣₗ Δ n a) = Δ
• SplitCut.f (SplitCut.RuleApp.axᵣᵣ Δ n a) = Δ
• SplitCut.f (SplitCut.RuleApp.andₗ Δ A B a) = Δ
• SplitCut.f (SplitCut.RuleApp.andᵣ Δ A B a) = Δ
• SplitCut.f (SplitCut.RuleApp.orₗ Δ A B a) = Δ
• SplitCut.f (SplitCut.RuleApp.orᵣ Δ A B a) = Δ
• SplitCut.f (SplitCut.RuleApp.boxₗ Δ A a) = Δ
• SplitCut.f (SplitCut.RuleApp.boxᵣ Δ A a) = Δ

def SplitCut.fₙ : RuleApp → SplitSequent

Given a RuleApp, obtain the non-principal formulas.

Equations

• SplitCut.fₙ r = SplitCut.f r \ SplitCut.fₚ r

theorem SplitCut.fₙ_alternate (r : RuleApp) : fₙ r = match r with | RuleApp.skp Δ => Δ | RuleApp.cutₗ Δ A => Δ | RuleApp.cutᵣ Δ A => Δ | RuleApp.wkₗ Δ A a => Δ \ {Sum.inl A} | RuleApp.wkᵣ Δ A a => Δ \ {Sum.inr A} | RuleApp.topₗ Δ a => Δ \ {Sum.inl ⊤} | RuleApp.topᵣ Δ a => Δ \ {Sum.inr ⊤} | RuleApp.axₗₗ Δ n a => Δ \ {Sum.inl (at n), Sum.inl (na n)} | RuleApp.axₗᵣ Δ n a => Δ \ {Sum.inl (at n), Sum.inr (na n)} | RuleApp.axᵣₗ Δ n a => Δ \ {Sum.inr (at n), Sum.inl (na n)} | RuleApp.axᵣᵣ Δ n a => Δ \ {Sum.inr (at n), Sum.inr (na n)} | RuleApp.andₗ Δ A B a => Δ \ {Sum.inl (A&B)} | RuleApp.andᵣ Δ A B a => Δ \ {Sum.inr (A&B)} | RuleApp.orₗ Δ A B a => Δ \ {Sum.inl (A v B)} | RuleApp.orᵣ Δ A B a => Δ \ {Sum.inr (A v B)} | RuleApp.boxₗ Δ A a => Δ \ {Sum.inl (□A)} | RuleApp.boxᵣ Δ A a => Δ \ {Sum.inr (□A)}

Relating principal formulas, non-principal formulas, and the split sequent.

def SplitCut.RuleApp.isBox : RuleApp → Prop

Equations

• (SplitCut.RuleApp.boxₗ Δ A a).isBox = (true = true)
• (SplitCut.RuleApp.boxᵣ Δ A a).isBox = (true = true)
• x✝.isBox = (false = true)

def SplitCut.r {X : Type} (α : X → T.obj X) (x : X) : RuleApp

Get RuleApp of a node (first projection).

Equations

• SplitCut.r α x = (α x).1

def SplitCut.p {X : Type} (α : X → T.obj X) (x : X) : List X

Get premises of a node (second projection).

Equations

• SplitCut.p α x = (α x).2

def SplitCut.edge {X : Type} (α : X → T.obj X) (x y : X) : Prop

Edge relation induced by p.

Equations

• SplitCut.edge α x y = (y ∈ SplitCut.p α x)

structure SplitCut.Proof : Type 1

Defininion of GL-ext proof.

• X : Type
• α : self.X → T.obj self.X
• step (x : self.X) : match r self.α x with | RuleApp.skp Δ => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [f (r self.α x)] | RuleApp.cutₗ Δ A => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).filterRight ∪ {Sum.inl A}, (fₙ (r self.α x)).filterLeft ∪ {Sum.inr (~A)}] | RuleApp.cutᵣ Δ A => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).filterLeft ∪ {Sum.inr A}, (fₙ (r self.α x)).filterRight ∪ {Sum.inl (~A)}] | RuleApp.wkₗ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x)] | RuleApp.wkᵣ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x)] | RuleApp.topₗ Δ a => p self.α x = ∅ | RuleApp.topᵣ Δ a => p self.α x = ∅ | RuleApp.axₗₗ Δ n a => p self.α x = ∅ | RuleApp.axₗᵣ Δ n a => p self.α x = ∅ | RuleApp.axᵣₗ Δ n a => p self.α x = ∅ | RuleApp.axᵣᵣ Δ n a => p self.α x = ∅ | RuleApp.andₗ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inl A}, fₙ (r self.α x) ∪ {Sum.inl B}] | RuleApp.andᵣ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inr A}, fₙ (r self.α x) ∪ {Sum.inr B}] | RuleApp.orₗ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inl A, Sum.inl B}] | RuleApp.orᵣ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inr A, Sum.inr B}] | RuleApp.boxₗ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {Sum.inl A}] | RuleApp.boxᵣ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {Sum.inr A}]
• path (x : self.X) (f : { f : ℕ → self.X // f 0 = x ∧ ∀ (n : ℕ), edge self.α (f n) (f (n + 1)) }) (n : ℕ) : ∃ (m : ℕ), (r self.α (↑f (n + m))).isBox

def SplitCut.proves (𝕏 : Proof) (Δ : SplitSequent) : Prop

Equations

• (𝕏⊢Δ) = ∃ (x : 𝕏.X), SplitCut.f (SplitCut.r 𝕏.α x) = Δ

def SplitCut.SplitSequent.isTrue (Δ : SplitSequent) : Prop

Equations

• (⊢Δ) = ∃ (𝕏 : SplitCut.Proof), 𝕏⊢Δ

def SplitCut.«term_⊢_» : Lean.TrailingParserDescr

Equations

• SplitCut.«term_⊢_» = Lean.ParserDescr.trailingNode `SplitCut.«term_⊢_» 6 7 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢") (Lean.ParserDescr.cat `term 6))

def SplitCut.«term⊢_» : Lean.ParserDescr

Equations

• SplitCut.«term⊢_» = Lean.ParserDescr.node `SplitCut.«term⊢_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢") (Lean.ParserDescr.cat `term 40))