Equations
- LO.Modal.Standard.«term_ᵇ» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.term_ᵇ 90 90 (Lean.ParserDescr.symbol "ᵇ")
Instances For
class
LO.Modal.Standard.BoxdotProperty
{α : Type u_1}
(Λ₁ : LO.Modal.Standard.DeductionParameter α)
(Λ₂ : LO.Modal.Standard.DeductionParameter α)
:
- bdp : ∀ {p : LO.Modal.Standard.Formula α}, Λ₁ ⊢! p ↔ Λ₂ ⊢! pᵇ
Instances
theorem
LO.Modal.Standard.BoxdotProperty.bdp
{α : Type u_1}
{Λ₁ : LO.Modal.Standard.DeductionParameter α}
{Λ₂ : LO.Modal.Standard.DeductionParameter α}
[self : LO.Modal.Standard.BoxdotProperty Λ₁ Λ₂]
{p : LO.Modal.Standard.Formula α}
:
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ᵇ)
:
theorem
LO.Modal.Standard.boxdotTranslatedK4_of_S4
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.iff_boxdotTranslation_S4
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.S4_of_boxdotTranslatedK4
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
(h : 𝐊𝟒 ⊢! pᵇ)
:
theorem
LO.Modal.Standard.iff_S4_boxdotTranslatedK4
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
Equations
- LO.Modal.Standard.instBoxdotPropertyS4K4 = { bdp := ⋯ }