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

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

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

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

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

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

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

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