Defining GL-split proof systems.

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

Basic components of the GL-split proof system.

inductive Split.RuleApp : Type

Rule applications for the GL-split proof system.

• 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 Split.T : CategoryTheory.Functor Type Type

Endofunctor for the GL-split proof system.

Equations

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

def Split.fₚ : RuleApp → SplitSequent

Given a RuleApp, obtain the principal formulas.

Equations

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

def Split.f : RuleApp → SplitSequent

Given a RuleApp, obtain the split sequent.

Equations

• Split.f (Split.RuleApp.topₗ Δ a) = Δ
• Split.f (Split.RuleApp.topᵣ Δ a) = Δ
• Split.f (Split.RuleApp.axₗₗ Δ n a) = Δ
• Split.f (Split.RuleApp.axₗᵣ Δ n a) = Δ
• Split.f (Split.RuleApp.axᵣₗ Δ n a) = Δ
• Split.f (Split.RuleApp.axᵣᵣ Δ n a) = Δ
• Split.f (Split.RuleApp.andₗ Δ A B a) = Δ
• Split.f (Split.RuleApp.andᵣ Δ A B a) = Δ
• Split.f (Split.RuleApp.orₗ Δ A B a) = Δ
• Split.f (Split.RuleApp.orᵣ Δ A B a) = Δ
• Split.f (Split.RuleApp.boxₗ Δ A a) = Δ
• Split.f (Split.RuleApp.boxᵣ Δ A a) = Δ

def Split.fₙ : RuleApp → SplitSequent

Given a RuleApp, obtain the non-principal formulas.

Equations

• Split.fₙ Γ = Split.f Γ \ Split.fₚ Γ

theorem Split.fₙ_alternate (r : RuleApp) : fₙ r = match r with | 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 sequent.

theorem Split.fₙ_sub_f {r : RuleApp} : fₙ r ⊆ f r

def Split.RuleApp.isBox : RuleApp → Prop

Equations

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

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

Get RuleApp of a node (first projection).

Equations

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

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

Get premises of a node (second projection).

Equations

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

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

Edge relation induced by p.

Equations

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

structure Split.Proof : Type 1

Defininion of GL-split proof.

• X : Type
• α : self.X → T.obj self.X
• step (x : self.X) : match r self.α x with | 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}]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Split.equiv (φ ψ : Formula) : Prop

Equations

• (φ≅ψ) = ((∃ (𝕏 : Split.Proof), 𝕏⊢{Sum.inl (~ψ), Sum.inr φ}) ∧ ∃ (𝕏 : Split.Proof), 𝕏⊢{Sum.inr ψ, Sum.inl (~φ)})

def Split.«term_≅_» : Lean.TrailingParserDescr

Equations

• Split.«term_≅_» = Lean.ParserDescr.trailingNode `Split.«term_≅_» 7 8 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "≅") (Lean.ParserDescr.cat `term 7))

Fischer-Ladner properties of GL-split proofs

theorem Split.edge_in_FL {𝕏 : Proof} {x y : 𝕏.X} (x_y : edge 𝕏.α x y) : f (r 𝕏.α y) ⊆ (f (r 𝕏.α x)).FL

Every edge is contained in FL closure.

theorem Split.path_in_FL {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) : f (r 𝕏.α y) ⊆ (f (r 𝕏.α x)).FL

Every path is contained in FL closure.

Point Generated GL-split Proofs

def Split.αPoint (𝕐 : Proof) (x : 𝕐.X) : { y : 𝕐.X // Relation.ReflTransGen (edge 𝕐.α) x y } → T.obj { y : 𝕐.X // Relation.ReflTransGen (edge 𝕐.α) x y }

Structure morphism for Point Generation.

Equations

• Split.αPoint 𝕐 x y = ((𝕐.α ↑y).1, List.pmap (fun (x_1 : 𝕐.X) (y : Relation.ReflTransGen (Split.edge 𝕐.α) x x_1) => ⟨x_1, y⟩) (𝕐.α ↑y).2 ⋯)

def Split.pointGeneratedProof (𝕐 : Proof) (x : 𝕐.X) : Proof

Point Generated Split Proof.

Equations

• Split.pointGeneratedProof 𝕐 x = { X := { y : 𝕐.X // Relation.ReflTransGen (Split.edge 𝕐.α) x y }, α := Split.αPoint 𝕐 x, step := ⋯ }

theorem Split.node_in_pg_sequent_in_FL (𝕏 : Proof) (x : 𝕏.X) (y : (pointGeneratedProof 𝕏 x).X) : f (r (αPoint 𝕏 x) y) ⊆ (f (r 𝕏.α x)).FL

Filtration of GL-Proofs

instance Split.instSetoidX (𝕏 : Proof) : Setoid 𝕏.X

Equivelance relation used for Filtration.

Equations

• Split.instSetoidX 𝕏 = { r := fun (x y : 𝕏.X) => Split.f (Split.r 𝕏.α x) = Split.f (Split.r 𝕏.α y), iseqv := ⋯ }

noncomputable def Split.αQuot (𝕐 : Proof) (x : Quotient (instSetoidX 𝕐)) : T.obj (Quotient (instSetoidX 𝕐))

Structure morphism for Filtration.

Equations

• Split.αQuot 𝕐 x = Split.T.map (Quotient.mk (Split.instSetoidX 𝕐)) (𝕐.α x.out)

noncomputable def Split.filtration (𝕐 : Proof) : Proof

Filtration of a GL-split Proof is a GL-split proof.

Equations

• Split.filtration 𝕐 = { X := Quotient (Split.instSetoidX 𝕐), α := Split.αQuot 𝕐, step := ⋯ }

Finite Model Property

theorem Split.finite_proof_of_proof (𝕏 : Proof) (Δ : SplitSequent) : (𝕏⊢Δ) → ∃ (𝕐 : Proof), Finite 𝕐.X ∧ (𝕐⊢Δ)

Given a split proof of Δ there exists a finite split proof of Δ

Properties of (infinite) paths

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

Equations

• Split.nbEdge α x y = (y ∈ Split.p α x ∧ ¬(Split.r α x).isBox)

theorem Split.lt_if_not_box_edge {𝕏 : Proof} {x y : 𝕏.X} (x_y : nbEdge 𝕏.α x y) : (f (r 𝕏.α y)).length < (f (r 𝕏.α x)).length

Non box edges reduce sequent size.

theorem Split.lt_if_not_box_path {𝕏 : Proof} {x y : 𝕏.X} : Relation.TransGen (nbEdge 𝕏.α) x y → (f (r 𝕏.α y)).length < (f (r 𝕏.α x)).length

Non box paths reduce sequent size.

theorem Split.no_non_box_loop {𝕏 : Proof} (x : 𝕏.X) : ¬Relation.TransGen (nbEdge 𝕏.α) x x

Non box paths do not loop.

theorem Split.exists_box_on_le_path {𝕏 : Proof} (x y : 𝕏.X) : Relation.TransGen (edge 𝕏.α) x y → (f (r 𝕏.α x)).length ≤ (f (r 𝕏.α y)).length → ∃ (z : 𝕏.X), Relation.ReflTransGen (edge 𝕏.α) x z ∧ Relation.ReflTransGen (edge 𝕏.α) z y ∧ (r 𝕏.α z).isBox

Every path of increasing size has a box rule application.

theorem Split.exists_box_on_loop {𝕏 : Proof} (x : 𝕏.X) : Relation.TransGen (edge 𝕏.α) x x → ∃ (z : 𝕏.X), Relation.ReflTransGen (edge 𝕏.α) x z ∧ Relation.ReflTransGen (edge 𝕏.α) z x ∧ (r 𝕏.α z).isBox

Every loop has a box edge.

def Split.edgeRestr {𝕏 : Proof} (p : 𝕏.X → Prop) : 𝕏.X → 𝕏.X → Prop

Edge relation restricted to nodes satisfying predicate p.

Equations

• Split.edgeRestr p x y = (Split.edge 𝕏.α x y ∧ p x ∧ p y)

theorem Split.exists_box_on_le_restr_path {𝕏 : Proof} (x y : 𝕏.X) (p : 𝕏.X → Prop) : Relation.TransGen (edgeRestr p) x y → (f (r 𝕏.α x)).length ≤ (f (r 𝕏.α y)).length → ∃ (z : 𝕏.X), Relation.ReflTransGen (edgeRestr p) x z ∧ Relation.TransGen (edgeRestr p) z y ∧ (r 𝕏.α z).isBox

Every restricted path of increasing size has a box rule application.

theorem Split.exists_box_on_restr_loop {𝕏 : Proof} (x : 𝕏.X) (p : 𝕏.X → Prop) : Relation.TransGen (edgeRestr p) x x → ∃ (z : 𝕏.X), (r 𝕏.α z).isBox ∧ p z ∧ Relation.TransGen (edgeRestr p) z z

Every restricted loop has a box edge.

theorem Split.inf_path_has_inf_boxes {𝕏 : Proof} (g : ℕ → 𝕏.X) (h : ∀ (n : ℕ), edge 𝕏.α (g n) (g (n + 1))) (n : ℕ) : ∃ (m : ℕ), (r 𝕏.α (g (n + m))).isBox

Every infinite path has an infinite number of nodes which are box rule applications.

theorem Split.finite_and_no_loop_implies_exists_leaf {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (h : 𝕏.X → Prop) (x : 𝕏.X) (x_sat : h x) : (¬∃ (y : 𝕏.X), Relation.TransGen (edgeRestr h) y y) → ∃ (y : 𝕏.X), h y ∧ ∀ z ∈ p 𝕏.α y, ¬h z

If a proof is finite and there are no loops under a restriction, then there must exist a leaf.

theorem Split.in_vocab_of_path_left {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) {n : ℕ} (n_in : n ∈ (f (r 𝕏.α y)).left.vocab) : n ∈ (f (r 𝕏.α x)).left.vocab

theorem Split.in_vocab_of_path_right {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) {n : ℕ} (n_in : n ∈ (f (r 𝕏.α y)).right.vocab) : n ∈ (f (r 𝕏.α x)).right.vocab