Documentation

ProvabilityLogic.LabelledGentzen.GLPoint3.Basic

Labelled sequent calculus for LogicGLPoint3, extending the calculus for GL with the linearity rule Lin. Original to this formalization, applying the method of [Neg14] — read a frame condition off as a structural rule — to weak connectedness.

[Neg14, §5]

inductive LogicGLPoint3.ProofLabelledGentzen {α : Type u} [DecidableEq α] :

LabelledSequent α → Type u

axm {α : Type u} [DecidableEq α] (x : Label) (A : Formula α) : ⊢ˡᵍ[GLPoint3]! (∅ ⸴ {x ∶ A} ⟹ˡ {x ∶ A})
botL {α : Type u} [DecidableEq α] (x : Label) : ⊢ˡᵍ[GLPoint3]! (∅ ⸴ {x ∶ ⊥} ⟹ˡ ∅)
wkRel {α : Type u} [DecidableEq α] {R R' : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} : ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ) → autoParam (R ⊆ R') _auto_1 → ⊢ˡᵍ[GLPoint3]! (R' ⸴ ℓΓ ⟹ˡ ℓΔ)
wkAnt {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΓ' ℓΔ : Finset (LabelledFormula α)} : ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ) → autoParam (ℓΓ ⊆ ℓΓ') _auto_3 → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ' ⟹ˡ ℓΔ)
wkSuc {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ ℓΔ' : Finset (LabelledFormula α)} : ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ) → autoParam (ℓΔ ⊆ ℓΔ') _auto_5 → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ')
impL {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} : ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A) ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ insert (x ∶ B) ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ insert (x ∶ A 🡒 B) ℓΓ ⟹ˡ ℓΔ)
impR {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} : ⊢ˡᵍ[GLPoint3]! (R ⸴ insert (x ∶ A) ℓΓ ⟹ˡ insert (x ∶ B) ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A 🡒 B) ℓΔ)
boxL {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (x y : Label) (A : Formula α) (hxy : (x, y) ∈ R := by grind) (hxA : x ∶ □A ∈ ℓΓ := by grind) : ⊢ˡᵍ[GLPoint3]! (R ⸴ insert (y ∶ A) ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ)
boxRLob {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (x y : Label) (A : Formula α) (hfresh : y ∉ (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ).labels := by grind) : ⊢ˡᵍ[GLPoint3]! (insert (x, y) R ⸴ insert (y ∶ □A) ℓΓ ⟹ˡ insert (y ∶ A) ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ)
irref {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (x : Label) (h : (x, x) ∈ R := by grind) : ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ)
trans {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (x y z : Label) (hxy : (x, y) ∈ R := by grind) (hyz : (y, z) ∈ R := by grind) : ⊢ˡᵍ[GLPoint3]! (insert (x, z) R ⸴ ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ)
lin {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (x y z : Label) (hxy : (x, y) ∈ R := by grind) (hxz : (x, z) ∈ R := by grind) : ⊢ˡᵍ[GLPoint3]! (insert (y, z) R ⸴ ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! (insert (z, y) R ⸴ ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! LabelledSequent.relabel y z (R ⸴ ℓΓ ⟹ˡ ℓΔ) → ⊢ˡᵍ[GLPoint3]! (R ⸴ ℓΓ ⟹ˡ ℓΔ)

Instances For

def LogicGLPoint3.«term⊢ˡᵍ[GLPoint3]!_» :

Lean.ParserDescr

Equations

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

Instances For

@[reducible, inline]

abbrev LogicGLPoint3.ProvableLabelledGentzen {α : Type u} [DecidableEq α] (S : LabelledSequent α) :

Equations

⊢ˡᵍ[GLPoint3] S = Nonempty (⊢ˡᵍ[GLPoint3]! S)

Instances For

def LogicGLPoint3.«term⊢ˡᵍ[GLPoint3]_» :

Lean.ParserDescr

Equations

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

Instances For

def LogicGLPoint3.«term⊬ˡᵍ[GLPoint3]_» :

Lean.ParserDescr

Equations

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

Instances For

theorem LogicGLPoint3.ProvableLabelledGentzen.axm {α : Type u} [DecidableEq α] (x : Label) (A : Formula α) :

⊢ˡᵍ[GLPoint3] (∅ ⸴ {x ∶ A} ⟹ˡ {x ∶ A})

theorem LogicGLPoint3.ProvableLabelledGentzen.botL {α : Type u} [DecidableEq α] (x : Label) :

⊢ˡᵍ[GLPoint3] (∅ ⸴ {x ∶ ⊥} ⟹ˡ ∅)

theorem LogicGLPoint3.ProvableLabelledGentzen.wkRel {α : Type u} [DecidableEq α] {R R' : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (hR : R ⊆ R') :

⊢ˡᵍ[GLPoint3] (R' ⸴ ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.wkAnt {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΓ' ℓΔ : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (hΓ : ℓΓ ⊆ ℓΓ') :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ' ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.wkSuc {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ ℓΔ' : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (hΔ : ℓΔ ⊆ ℓΔ') :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ')

theorem LogicGLPoint3.ProvableLabelledGentzen.impL {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} (h₁ : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A) ℓΔ)) (h₂ : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (x ∶ B) ℓΓ ⟹ˡ ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ insert (x ∶ A 🡒 B) ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.impR {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (x ∶ A) ℓΓ ⟹ˡ insert (x ∶ B) ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A 🡒 B) ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.boxL {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y : Label} {A : Formula α} (hxy : (x, y) ∈ R := by grind) (hxA : x ∶ □A ∈ ℓΓ := by grind) (h : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (y ∶ A) ℓΓ ⟹ˡ ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.boxRLob {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y : Label} {A : Formula α} (hfresh : y ∉ (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ).labels := by grind) (h : ⊢ˡᵍ[GLPoint3] (insert (x, y) R ⸴ insert (y ∶ □A) ℓΓ ⟹ˡ insert (y ∶ A) ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.irref {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} (h : (x, x) ∈ R := by grind) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.trans {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y z : Label} (hxy : (x, y) ∈ R := by grind) (hyz : (y, z) ∈ R := by grind) (h : ⊢ˡᵍ[GLPoint3] (insert (x, z) R ⸴ ℓΓ ⟹ˡ ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.lin {α : Type u} [DecidableEq α] {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y z : Label} (hxy : (x, y) ∈ R := by grind) (hxz : (x, z) ∈ R := by grind) (h₁ : ⊢ˡᵍ[GLPoint3] (insert (y, z) R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h₂ : ⊢ˡᵍ[GLPoint3] (insert (z, y) R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h₃ : ⊢ˡᵍ[GLPoint3] LabelledSequent.relabel y z (R ⸴ ℓΓ ⟹ˡ ℓΔ)) :

⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)

theorem LogicGLPoint3.ProvableLabelledGentzen.rec {α : Type u} [DecidableEq α] {motive : (S : LabelledSequent α) → ⊢ˡᵍ[GLPoint3] S → Prop} (axm : ∀ (x : Label) (A : Formula α), motive (∅ ⸴ {x ∶ A} ⟹ˡ {x ∶ A}) ⋯) (botL : ∀ (x : Label), motive (∅ ⸴ {x ∶ ⊥} ⟹ˡ ∅) ⋯) (wkRel : ∀ {R R' : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h' : R ⊆ R'), motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) h → motive (R' ⸴ ℓΓ ⟹ˡ ℓΔ) ⋯) (wkAnt : ∀ {R : Finset LabelRel} {ℓΓ ℓΓ' ℓΔ : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h' : ℓΓ ⊆ ℓΓ'), motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) h → motive (R ⸴ ℓΓ' ⟹ˡ ℓΔ) ⋯) (wkSuc : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ ℓΔ' : Finset (LabelledFormula α)} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h' : ℓΔ ⊆ ℓΔ'), motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) h → motive (R ⸴ ℓΓ ⟹ˡ ℓΔ') ⋯) (impL : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} (h₁ : ⊢ˡᵍ[GLPoint3] (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A) ℓΔ)) (h₂ : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (x ∶ B) ℓΓ ⟹ˡ ℓΔ)), motive (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A) ℓΔ) h₁ → motive (R ⸴ insert (x ∶ B) ℓΓ ⟹ˡ ℓΔ) h₂ → motive (R ⸴ insert (x ∶ A 🡒 B) ℓΓ ⟹ˡ ℓΔ) ⋯) (impR : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} {A B : Formula α} (h : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (x ∶ A) ℓΓ ⟹ˡ insert (x ∶ B) ℓΔ)), motive (R ⸴ insert (x ∶ A) ℓΓ ⟹ˡ insert (x ∶ B) ℓΔ) h → motive (R ⸴ ℓΓ ⟹ˡ insert (x ∶ A 🡒 B) ℓΔ) ⋯) (boxL : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y : Label} {A : Formula α} (hxy : (x, y) ∈ R) (hxA : x ∶ □A ∈ ℓΓ) (h : ⊢ˡᵍ[GLPoint3] (R ⸴ insert (y ∶ A) ℓΓ ⟹ˡ ℓΔ)), motive (R ⸴ insert (y ∶ A) ℓΓ ⟹ˡ ℓΔ) h → motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) ⋯) (boxRLob : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y : Label} {A : Formula α} (hfresh : y ∉ (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ).labels) (h : ⊢ˡᵍ[GLPoint3] (insert (x, y) R ⸴ insert (y ∶ □A) ℓΓ ⟹ˡ insert (y ∶ A) ℓΔ)), motive (insert (x, y) R ⸴ insert (y ∶ □A) ℓΓ ⟹ˡ insert (y ∶ A) ℓΔ) h → motive (R ⸴ ℓΓ ⟹ˡ insert (x ∶ □A) ℓΔ) ⋯) (irref : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x : Label} (h : (x, x) ∈ R), motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) ⋯) (trans : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y z : Label} (hxy : (x, y) ∈ R) (hyz : (y, z) ∈ R) (h : ⊢ˡᵍ[GLPoint3] (insert (x, z) R ⸴ ℓΓ ⟹ˡ ℓΔ)), motive (insert (x, z) R ⸴ ℓΓ ⟹ˡ ℓΔ) h → motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) ⋯) (lin : ∀ {R : Finset LabelRel} {ℓΓ ℓΔ : Finset (LabelledFormula α)} {x y z : Label} (hxy : (x, y) ∈ R) (hxz : (x, z) ∈ R) (h₁ : ⊢ˡᵍ[GLPoint3] (insert (y, z) R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h₂ : ⊢ˡᵍ[GLPoint3] (insert (z, y) R ⸴ ℓΓ ⟹ˡ ℓΔ)) (h₃ : ⊢ˡᵍ[GLPoint3] LabelledSequent.relabel y z (R ⸴ ℓΓ ⟹ˡ ℓΔ)), motive (insert (y, z) R ⸴ ℓΓ ⟹ˡ ℓΔ) h₁ → motive (insert (z, y) R ⸴ ℓΓ ⟹ˡ ℓΔ) h₂ → motive (LabelledSequent.relabel y z (R ⸴ ℓΓ ⟹ˡ ℓΔ)) h₃ → motive (R ⸴ ℓΓ ⟹ˡ ℓΔ) ⋯) {S : LabelledSequent α} (h : ⊢ˡᵍ[GLPoint3] S) :

motive S h