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

Equations

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

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

Equations

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

theorem LO.Modal.Standard.Formula.BoxdotTranslation.top_def {α : Type u_1} : ⊤ᵇ = ⊤

theorem LO.Modal.Standard.Formula.BoxdotTranslation.box_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} : (□p)ᵇ = ⊡pᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.imp_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : (p ⟶ q)ᵇ = pᵇ ⟶ qᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.neg_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} : (~p)ᵇ = ~pᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.and_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : (p ⋏ q)ᵇ = pᵇ ⋏ qᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.or_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : (p ⋎ q)ᵇ = pᵇ ⋎ qᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.iff_def {α : Type u_1} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : (p ⟷ q)ᵇ = pᵇ ⟷ qᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.axiomK {α : Type u_1} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : LO.Axioms.K p qᵇ = ⊡(pᵇ ⟶ qᵇ) ⟶ ⊡pᵇ ⟶ ⊡qᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.axiomT {α : Type u_1} {p : LO.Modal.Standard.Formula α} : LO.Axioms.T pᵇ = ⊡pᵇ ⟶ pᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.axiomFour {α : Type u_1} {p : LO.Modal.Standard.Formula α} : LO.Axioms.Four pᵇ = ⊡pᵇ ⟶ ⊡⊡pᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.axiomL {α : Type u_1} {p : LO.Modal.Standard.Formula α} : LO.Axioms.L pᵇ = ⊡(⊡pᵇ ⟶ pᵇ) ⟶ ⊡pᵇ

theorem LO.Modal.Standard.Formula.BoxdotTranslation.axiomGrz {α : Type u_1} {p : LO.Modal.Standard.Formula α} : LO.Axioms.Grz pᵇ = ⊡(⊡(pᵇ ⟶ ⊡pᵇ) ⟶ pᵇ) ⟶ pᵇ

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

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

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

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

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

theorem LO.Modal.Standard.boxdotTranslatedGL_of_Grz {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐆𝐫𝐳 ⊢! p → 𝐆𝐋 ⊢! pᵇ