theorem LO.Modal.Hilbert.Triv.unprovable_AxiomL {a : ℕ} : LO.Modal.Hilbert.Triv ℕ ⊬ LO.Axioms.L (LO.Modal.Formula.atom a)

theorem LO.Modal.Hilbert.Ver.unprovable_AxiomP : LO.Modal.Hilbert.Ver ℕ ⊬ LO.Axioms.P

theorem LO.Modal.Hilbert.K4.provable_Cl_trivTranslated {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.K4 α ⊢! φ → LO.IntProp.Hilbert.Cl α ⊢! (φᵀᴾ) ⋯

theorem LO.Modal.Hilbert.K4.unprovable_AxiomL {a : ℕ} : LO.Modal.Hilbert.K4 ℕ ⊬ LO.Axioms.L (LO.Modal.Formula.atom a)

theorem LO.Modal.Hilbert.GL.provable_CL_verTranslated {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.GL α ⊢! φ → LO.IntProp.Hilbert.Cl α ⊢! (φⱽᴾ) ⋯

theorem LO.Modal.Hilbert.GL.unprovable_AxiomT {a : ℕ} : LO.Modal.Hilbert.GL ℕ ⊬ LO.Axioms.T (LO.Modal.Formula.atom a)

instance LO.Modal.Hilbert.GL.instConsistentFormulaNat : LO.System.Consistent (LO.Modal.Hilbert.GL ℕ)

Equations

• LO.Modal.Hilbert.GL.instConsistentFormulaNat = ⋯

theorem LO.Modal.Hilbert.not_S4_weakerThan_GL : ¬LO.Modal.Hilbert.S4 ℕ ≤ₛ LO.Modal.Hilbert.GL ℕ