Defining GL-proof systems.

Here we define the GL-proof system along with finitization and basic properties.

Basic components of the GL-proof system.

inductive RuleApp : Type

Rule applications for the GL-proof system.

• top (Δ : Sequent) : ⊤ ∈ Δ → RuleApp
• ax (Δ : Sequent) (n : ℕ) : at n ∈ Δ ∧ na n ∈ Δ → RuleApp
• and (Δ : Sequent) (φ ψ : Formula) : (φ&ψ) ∈ Δ → RuleApp
• or (Δ : Sequent) (φ ψ : Formula) : (φ v ψ) ∈ Δ → RuleApp
• box (Δ : Sequent) (φ : Formula) : □φ ∈ Δ → RuleApp

def T : CategoryTheory.Functor Type Type

Endofunctor for the GL-proof system.

Equations

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

def fₚ : RuleApp → Sequent

Given a RuleApp, obtain the principal formulas.

Equations

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

def f : RuleApp → Sequent

Given a RuleApp, obtain the sequent.

Equations

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

def fₙ : RuleApp → Sequent

Given a RuleApp, obtain the non-principal formulas.

Equations

• fₙ r = f r \ fₚ r

theorem fₙ_alternate (r : RuleApp) : fₙ r = match r with | RuleApp.top Δ a => Δ \ {⊤} | RuleApp.ax Δ n a => Δ \ {at n, na n} | RuleApp.and Δ A B a => Δ \ {A&B} | RuleApp.or Δ A B a => Δ \ {A v B} | RuleApp.box Δ A a => Δ \ {□A}

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

theorem fₚ_sub_f {r : RuleApp} : fₚ r ⊆ f r

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

def RuleApp.isBox : RuleApp → Bool

Equations

• (RuleApp.box Δ φ a).isBox = true
• x✝.isBox = false

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

Get RuleApp of a node (first projection).

Equations

• r α x = (α x).1

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

Get premises of a node (second projection).

Equations

• p α x = (α x).2

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

Edge relation induced by p.

Equations

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

structure Proof : Type 1

Defininion of GL-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.ax Δ n a => p self.α x = [] | RuleApp.and Δ φ ψ a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {φ}, fₙ (r self.α x) ∪ {ψ}] | RuleApp.or Δ φ ψ a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {φ, ψ}] | RuleApp.box Δ φ a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {φ}]

def proves (𝕏 : Proof) (Δ : Sequent) : Prop

Equations

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

def Sequent.isTrue (Δ : Sequent) : Prop

Equations

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

def «term_⊢_» : Lean.TrailingParserDescr

Equations

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

def «term⊢_» : Lean.ParserDescr

Equations

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

theorem not_prove_empty : ¬∃ (𝕏 : Proof), 𝕏⊢∅

Fischer-Ladner properties of GL-proofs

theorem 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 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-Proofs

def α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

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

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

Point Generated Proof.

Equations

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

theorem 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 instSetoidX (𝕏 : Proof) : Setoid 𝕏.X

Equivelance relation used for Filtration.

Equations

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

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

Structure morphism for Filtration.

Equations

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

noncomputable def filtration (𝕐 : Proof) : Proof

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

Equations

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

Finite Model Property

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

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

Properties of (infinite) paths

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

Equations

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

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

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

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