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 Lean4GlCoalgebras.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 Lean4GlCoalgebras.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 Lean4GlCoalgebras.fₚ : RuleApp → Sequent

Given a RuleApp, obtain the principal formulas.

Equations

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

def Lean4GlCoalgebras.f : RuleApp → Sequent

Given a RuleApp, obtain the sequent.

Equations

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

def Lean4GlCoalgebras.fₙ : RuleApp → Sequent

Given a RuleApp, obtain the non-principal formulas.

Equations

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.fₚ_sub_f {r : RuleApp} : fₚ r ⊆ f r

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

def Lean4GlCoalgebras.RuleApp.isBox : RuleApp → Bool

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Get RuleApp of a node (first projection).

Equations

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

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

Get premises of a node (second projection).

Equations

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

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

Edge relation induced by p.

Equations

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

structure Lean4GlCoalgebras.Proof : Type 1

Definition of GL-proof.

• X : Type

  Auxiliary declaration used in the GL coalgebra development.

• α : self.X → T.obj self.X

  Auxiliary declaration used in the GL coalgebra development.

• 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 Lean4GlCoalgebras.Proof.toCoalgebra (𝕏 : Proof) : CategoryTheory.Endofunctor.Coalgebra T

GL-proofs are coalgebras. Note: we can do this the other way around, i.e. Proof extends CategoryTheory.Endofunctor.Coalgebra T, however I find X and α more explicative than V and str

Equations

• 𝕏.toCoalgebra = { V := 𝕏.X, str := TypeCat.ofHom 𝕏.α }

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

A proof 𝕏 proves sequent Δ if some node of 𝕏 has sequent Δ as its sequent.

Equations

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

def Lean4GlCoalgebras.Sequent.isTrue (Δ : Sequent) : Prop

A sequent is provable if there exists a GL-proof of it.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Fischer-Ladner properties of GL-proofs

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.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 Lean4GlCoalgebras.α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

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

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

Point Generated Proof.

Equations

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

theorem Lean4GlCoalgebras.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

@[implicit_reducible]

instance Lean4GlCoalgebras.fEqEquiRel (𝕏 : Proof) : Setoid 𝕏.X

Equivalence relation used for Filtration.

Equations

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

noncomputable def Lean4GlCoalgebras.αQuot (𝕐 : Proof) (x : Quotient (fEqEquiRel 𝕐)) : RuleApp × List (Quotient (fEqEquiRel 𝕐))

Structure morphism for Filtration.

Equations

• Lean4GlCoalgebras.αQuot 𝕐 x = ((𝕐.α x.out).1, List.map (Quotient.mk (Lean4GlCoalgebras.fEqEquiRel 𝕐)) (𝕐.α x.out).2)

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

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

Equations

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

Finite Proof Property

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

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

Properties of (infinite) paths

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

theorem Lean4GlCoalgebras.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.