The MM0 formal system

$$$$Gamma : = @ mid Gamma, x : s mid Gamma, \ * varphi : s * x """contexts"""

e : = x mid varphi mid t * e """expressions"""

A : = e, Delta : = A """statements"""

E : = delta """environment"""

delta : = (t) s * sort """sorts"""

mid t : Gamma Rightarrow s * x """terms"""

phantom(t) == (y : s__deriv) .e """definitions"""

mid axiom """axioms"""

mid thm """theorems""" """declarations"""

The MM0 formal system

$$$$V(x) ==(x)

V_Gamma(varphi) == x """(where(varphi : s x) in Gamma)"""

V(t * e) == (bigcup_i V(e_i))

4 pt FV(x) ==(x)

FV_Gamma(varphi) == x """(where(varphi : s x) in Gamma)"""

FV(t * e) == underline(FV(e : : Gamma__deriv)) * cup(e_i mid

Gamma__deriv_i in x) """(where t : Gamma__deriv Rightarrow s

x)"""

The MM0 formal system

$$$$underline(FV(@ : : @)) == emptyset

underline(FV(e, y : : Gamma__deriv, x : s)) == underline(FV(e

: : Gamma__deriv))

underline(FV(e, e__deriv : : Gamma__deriv, varphi : s * x))

== underline(FV(e : : Gamma__deriv)) * cup(FV(e__deriv) setminus(e_i

mid Gamma__deriv_i in x))

The MM0 formal system

$$$$Gamma : = @ mid Gamma, x : s mid Gamma, \ * varphi : s * x """contexts"""

e : = x mid varphi mid t * e """expressions"""

A : = e, Delta : = A """statements"""

E : = delta """environment"""

delta : = (t) s * sort """sorts"""

mid t : Gamma Rightarrow s * x """terms"""

phantom(t) == (y : s__deriv) .e """definitions"""

mid axiom """axioms"""

mid thm """theorems""" """declarations"""

The MM0 formal system

$$$$V(x) ==(x)

V_Gamma(varphi) == x """(where(varphi : s x) in Gamma)"""

V(t * e) == (bigcup_i V(e_i))

4 pt FV(x) ==(x)

FV_Gamma(varphi) == x """(where(varphi : s x) in Gamma)"""

FV(t * e) == underline(FV(e : : Gamma__deriv)) * cup(e_i mid

Gamma__deriv_i in x) """(where t : Gamma__deriv Rightarrow s

x)"""

The MM0 formal system

$$$$underline(FV(@ : : @)) == emptyset

underline(FV(e, y : : Gamma__deriv, x : s)) == underline(FV(e

: : Gamma__deriv))

underline(FV(e, e__deriv : : Gamma__deriv, varphi : s * x))

== underline(FV(e : : Gamma__deriv)) * cup(FV(e__deriv) setminus(e_i

mid Gamma__deriv_i in x))