Unnecessitation

theorem LO.Modal.Hilbert.GL.imply_boxdot_plain_of_imply_box_box {φ ψ : Formula ℕ} : Hilbert.GL ⊢! □φ ==> □ψ → Hilbert.GL ⊢! ⊡φ ==> ψ

theorem LO.Modal.Hilbert.GL.unnecessitation! {φ : Formula ℕ} : Hilbert.GL ⊢! □φ → Hilbert.GL ⊢! φ

@[implicit_reducible]

noncomputable instance LO.Modal.Hilbert.GL.instUnnecessitationNatFormula : Entailment.Unnecessitation Hilbert.GL

Equations

• LO.Modal.Hilbert.GL.instUnnecessitationNatFormula = { unnec := fun {φ : LO.Modal.Formula ℕ} (h : LO.Modal.Hilbert.GL ⊢ □φ) => Nonempty.some ⋯ }