Documentation

Foundation.Modal.System.K4

source
def LO.System.imply_BoxBoxdot_Box {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘βŠ‘Ο† ➝ β–‘Ο†
Equations
source
@[simp]
theorem LO.System.imply_boxboxdot_box {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! β–‘βŠ‘Ο† ➝ β–‘Ο†
source
def LO.System.imply_Box_BoxBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘Ο† ➝ β–‘βŠ‘Ο†
Equations
source
@[simp]
theorem LO.System.imply_box_boxboxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! β–‘Ο† ➝ β–‘βŠ‘Ο†
source
def LO.System.imply_Box_BoxBoxdot' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} (h : 𝓒 ⊒ β–‘Ο†) :
𝓒 ⊒ β–‘βŠ‘Ο†
Equations
source
def LO.System.imply_Box_BoxBoxdot'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} (h : 𝓒 ⊒! β–‘Ο†) :
𝓒 ⊒! β–‘βŠ‘Ο†
Equations
  • β‹― = β‹―
source
def LO.System.iff_Box_BoxBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘Ο† β­€ β–‘βŠ‘Ο†
Equations
source
@[simp]
theorem LO.System.iff_box_boxboxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! β–‘Ο† β­€ β–‘βŠ‘Ο†
source
def LO.System.iff_Box_BoxdotBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘Ο† β­€ βŠ‘β–‘Ο†
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem LO.System.iff_box_boxdotbox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! β–‘Ο† β­€ βŠ‘β–‘Ο†
source
def LO.System.iff_Boxdot_BoxdotBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ βŠ‘Ο† β­€ βŠ‘βŠ‘Ο†
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem LO.System.iff_boxdot_boxdotboxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! βŠ‘Ο† β­€ βŠ‘βŠ‘Ο†
source
def LO.System.boxdotAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒ βŠ‘Ο† ➝ βŠ‘βŠ‘Ο†
Equations
source
@[simp]
theorem LO.System.boxdot_axiomFour! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.K4 𝓒] {Ο† : F} :
𝓒 ⊒! βŠ‘Ο† ➝ βŠ‘βŠ‘Ο†