Unprovability

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 {φ : 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 {φ : 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 : Entailment.Consistent Hilbert.GL

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