def LO.Modal.Formula.BoxdotTranslation {α : Type u_1} : LO.Modal.Formula α → LO.Modal.Formula α

Equations

• LO.Modal.Formula.atom pᵇ = LO.Modal.Formula.atom p
• LO.Modal.Formula.falsumᵇ = ⊥
• p.imp qᵇ = pᵇ ➝ qᵇ
• p.boxᵇ = ⊡pᵇ

def LO.Modal.«term_ᵇ» : Lean.TrailingParserDescr

Equations

• LO.Modal.«term_ᵇ» = Lean.ParserDescr.trailingNode `LO.Modal.term_ᵇ 90 90 (Lean.ParserDescr.symbol "ᵇ")

class LO.Modal.BoxdotProperty {α : Type u_1} (Λ₁ : LO.Modal.Hilbert α) (Λ₂ : LO.Modal.Hilbert α) : Type

• bdp : ∀ {p : LO.Modal.Formula α}, Λ₁ ⊢! p ↔ Λ₂ ⊢! pᵇ

theorem LO.Modal.BoxdotProperty.bdp {α : Type u_1} {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [self : LO.Modal.BoxdotProperty Λ₁ Λ₂] {p : LO.Modal.Formula α} : Λ₁ ⊢! p ↔ Λ₂ ⊢! pᵇ

theorem LO.Modal.boxdotTranslated {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [Λ₁.IsNormal] [Λ₂.IsNormal] (h : ∀ p ∈ Ax(Λ₁), Λ₂ ⊢! pᵇ) : Λ₁ ⊢! p → Λ₂ ⊢! pᵇ

theorem LO.Modal.boxdotTranslatedK4_of_S4 {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} : 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ

theorem LO.Modal.iff_boxdotTranslation_S4 {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} : 𝐒𝟒 ⊢! p ⭤ pᵇ

theorem LO.Modal.S4_of_boxdotTranslatedK4 {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} (h : 𝐊𝟒 ⊢! pᵇ) : 𝐒𝟒 ⊢! p

theorem LO.Modal.iff_S4_boxdotTranslatedK4 {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} : 𝐒𝟒 ⊢! p ↔ 𝐊𝟒 ⊢! pᵇ

instance LO.Modal.instBoxdotPropertyS4K4 {α : Type u_1} [DecidableEq α] : LO.Modal.BoxdotProperty 𝐒𝟒 𝐊𝟒

Equations

• LO.Modal.instBoxdotPropertyS4K4 = { bdp := ⋯ }