Documentation

Foundation.Modal.Boxdot.K4_S4

source
theorem LO.Modal.boxdotTranslatedK4_of_S4 {α : Type u_1} [DecidableEq α] {φ : Formula α} :
Hilbert.S4 α ⊢! φ → Hilbert.K4 α ⊢! φᵇ
source
theorem LO.Modal.iff_boxdotTranslation_S4 {α : Type u_1} [DecidableEq α] {φ : Formula α} :
Hilbert.S4 α ⊢! φ ⭤ φᵇ
source
theorem LO.Modal.S4_of_boxdotTranslatedK4 {α : Type u_1} [DecidableEq α] {φ : Formula α} (h : Hilbert.K4 α ⊢! φᵇ) :
Hilbert.S4 α ⊢! φ
source
theorem LO.Modal.iff_S4_boxdotTranslatedK4 {α : Type u_1} [DecidableEq α] {φ : Formula α} :
Hilbert.K4 α ⊢! φᵇ ↔ Hilbert.S4 α ⊢! φ
source
instance LO.Modal.instBoxdotPropertyK4S4 {α : Type u_1} [DecidableEq α] :
BoxdotProperty (Hilbert.K4 α) (Hilbert.S4 α)