def LO.System.goedel2 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : 𝓢 ⊢ ∼□⊥ ⭤ ∼□(∼□⊥)

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.goedel2! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : 𝓢 ⊢! ∼□⊥ ⭤ ∼□(∼□⊥)

def LO.System.goedel2'.mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : 𝓢 ⊢ ∼□⊥ → 𝓢 ⊢ ∼□(∼□⊥)

Equations

• LO.System.goedel2'.mp h = LO.System.and₁' LO.System.goedel2⨀h

def LO.System.goedel2'.mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : 𝓢 ⊢ ∼□(∼□⊥) → 𝓢 ⊢ ∼□⊥

Equations

• LO.System.goedel2'.mpr h = LO.System.and₂' LO.System.goedel2⨀h

theorem LO.System.goedel2'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : 𝓢 ⊢! ∼□⊥ ↔ 𝓢 ⊢! ∼□(∼□⊥)

def LO.System.GL.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ : F} : 𝓢 ⊢ Axioms.Four φ

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.GL.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : HasAxiomFour 𝓢

Equations

• LO.System.GL.instHasAxiomFour = { Four := fun (x : F) => LO.System.GL.axiomFour }

instance LO.System.GL.instK4 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] : System.K4 𝓢

Equations

• LO.System.GL.instK4 = LO.System.K4.mk

def LO.System.GL.axiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ : F} : 𝓢 ⊢ Axioms.H φ

Equations

• LO.System.GL.axiomH = LO.System.impTrans'' (LO.System.implyBoxDistribute' LO.System.and₁) LO.System.axiomL

instance LO.System.GL.instHasAxiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.GL 𝓢] : HasAxiomH 𝓢

Equations

• LO.System.GL.instHasAxiomH = { H := fun (x : F) => LO.System.GL.axiomH }