theorem
LO.Modal.boxdotTranslatedK4_of_S4
{α : Type u_1}
[DecidableEq α]
{φ : LO.Modal.Formula α}
:
LO.Modal.Hilbert.S4 α ⊢! φ → LO.Modal.Hilbert.K4 α ⊢! φᵇ
theorem
LO.Modal.iff_boxdotTranslation_S4
{α : Type u_1}
[DecidableEq α]
{φ : LO.Modal.Formula α}
:
LO.Modal.Hilbert.S4 α ⊢! φ ⭤ φᵇ
theorem
LO.Modal.S4_of_boxdotTranslatedK4
{α : Type u_1}
[DecidableEq α]
{φ : LO.Modal.Formula α}
(h : LO.Modal.Hilbert.K4 α ⊢! φᵇ)
:
theorem
LO.Modal.iff_S4_boxdotTranslatedK4
{α : Type u_1}
[DecidableEq α]
{φ : LO.Modal.Formula α}
:
LO.Modal.Hilbert.K4 α ⊢! φᵇ ↔ LO.Modal.Hilbert.S4 α ⊢! φ
Equations
- ⋯ = ⋯