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

Equations

• LO.Modal.Formula.atom aᵇ = LO.Modal.Formula.atom a
• LO.Modal.Formula.falsumᵇ = ⊥
• φ.imp ψᵇ = φᵇ ➝ ψᵇ
• φ.boxᵇ = ⊡φᵇ

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} (H₁ H₂ : Hilbert α) : Prop

• bdp {φ : Formula α} : H₁ ⊢! φᵇ ↔ H₂ ⊢! φ

Instances

• LO.Modal.Hilbert.instBoxdotPropertyNatGLGrz
• LO.Modal.instBoxdotPropertyK4S4

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