def
LO.System.goedel2'.mp
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.GL π’]
:
Equations
def
LO.System.goedel2'.mpr
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.GL π’]
:
Equations
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
def
LO.System.GL.axiomH
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[System F S]
{π’ : S}
[System.GL π’]
{Ο : F}
:
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 }