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_trivTranslated_Cl {φ : Formula ℕ} : Hilbert.K4 ⊢! φ → Propositional.Hilbert.Cl ⊢! φᵀ.toPropFormula ⋯

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

theorem LO.Modal.Hilbert.GL.provable_verTranslated_Cl {φ : Formula ℕ} : Hilbert.GL ⊢! φ → Propositional.Hilbert.Cl ⊢! φⱽ.toPropFormula ⋯

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

instance LO.Modal.Hilbert.GL.instConsistentFormulaNat : Entailment.Consistent Hilbert.GL

theorem LO.Modal.Hilbert.not_S4_weakerThan_GL : ¬Hilbert.S4 ⪯ Hilbert.GL