The logic GL

@[reducible, inline]

abbrev FFL.ProvabilityLogic.Logic.GL {α : Type u_1} : Logic α

Equations

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

def FFL.ProvabilityLogic.«term𝐆𝐋» : Lean.ParserDescr

Equations

• FFL.ProvabilityLogic.«term𝐆𝐋» = Lean.ParserDescr.node `FFL.ProvabilityLogic.«term𝐆𝐋» 1024 (Lean.ParserDescr.symbol "𝐆𝐋")

@[simp]

theorem FFL.ProvabilityLogic.Logic.GL.axiom4 {α : Type u_1} {A : Formula α} : 𝐆𝐋 ⊢ □A 🡒 □□A

@[simp]

theorem FFL.ProvabilityLogic.Logic.GL.axiomL {α : Type u_1} {A : Formula α} : 𝐆𝐋 ⊢ □(□A 🡒 A) 🡒 □A

Kripke soundness

theorem FFL.ProvabilityLogic.Logic.GL.forces_axiomL {α : Type u_1} {A : Formula α} {κ : Type u_2} [Nonempty κ] {M : Kripke.Model κ α} [M.IsGL] {x : M.World} : Kripke.Model.World.Forces M x (□(□A 🡒 A) 🡒 □A)

theorem FFL.ProvabilityLogic.Logic.GL.sound {α : Type u_1} {A : Formula α} {κ : Type u_2} [Nonempty κ] (M : Kripke.Model κ α) [M.IsGL] (h : 𝐆𝐋 ⊢ A) : M ⊧ A

instance FFL.ProvabilityLogic.Logic.GL.instConsistentFormula {α : Type u_1} : Entailment.Consistent 𝐆𝐋

From the sequent calculus

theorem FFL.ProvabilityLogic.Logic.GL.of_gentzen {α : Type u_1} [DecidableEq α] {S : Sequent α} (h : ⊢ᴳ[𝐆𝐋] S) : 𝐆𝐋 ⊢ Finset.conj S.ant 🡒 Finset.disj S.suc

Quasi-normal extensions

theorem FFL.ProvabilityLogic.Logic.GL.sumQuasiNormal_of_conj {α : Type u_1} {A : Formula α} [DecidableEq α] {L : Logic α} {Γ : FormulaFinset α} (hΓ : ∀ B ∈ Γ, 𝐆𝐋 +ᴸ L ⊢ B) (h : 𝐆𝐋 ⊢ Finset.conj Γ 🡒 A) : 𝐆𝐋 +ᴸ L ⊢ A

Completeness

theorem FFL.ProvabilityLogic.Logic.GL.provability_TFAE {α : Type u} [DecidableEq α] {A : Formula α} : [𝐆𝐋 ⊢ A, ⊢ᴳ[𝐆𝐋] ∅ ⟹ {A}, ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.Model κ α) [M.IsFiniteGL], M ⊧ A, ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.RootedModel κ α) [M.IsFiniteGL], Kripke.Model.World.Forces M.toModel M.root A, ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.RootedModel κ α) [M.IsFiniteGL] [M.IsTree], Kripke.Model.World.Forces M.toModel M.root A].TFAE

theorem FFL.ProvabilityLogic.Logic.GL.iff_provable_gentzen {α : Type u} [DecidableEq α] {A : Formula α} : 𝐆𝐋 ⊢ A ↔ ⊢ᴳ[𝐆𝐋] ∅ ⟹ {A}

theorem FFL.ProvabilityLogic.Logic.GL.iff_valid_finite {α : Type u} {A : Formula α} : 𝐆𝐋 ⊢ A ↔ ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.Model κ α) [M.IsFiniteGL], M ⊧ A

theorem FFL.ProvabilityLogic.Logic.GL.iff_root_forces {α : Type u} {A : Formula α} : 𝐆𝐋 ⊢ A ↔ ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.RootedModel κ α) [M.IsFiniteGL], Kripke.Model.World.Forces M.toModel M.root A

theorem FFL.ProvabilityLogic.Logic.GL.iff_tree_root_forces {α : Type u} {A : Formula α} : 𝐆𝐋 ⊢ A ↔ ∀ {κ : Type u} [inst : Nonempty κ] (M : Kripke.RootedModel κ α) [M.IsFiniteGL] [M.IsTree], Kripke.Model.World.Forces M.toModel M.root A

• [CZ97]