X_C A \lhd A[G / X_C]$ if $G$ is a classical type.

If $A$ is a classical type and $A \lhd B$ (or $A \approx B$), then $B$ is a classical type.

**Proof Easy. $\Box$**

The logical properties of $M2$
------------------------------

We denote by $LAF2$, $LC2$, and $LM2$ the underlying logic systems of respectively $AF2$, $C2$, and $M2$ type systems.\
With each classical variable $X_C$, we associate a special variable $X^{\ast}$ of $AF2$ having the same arity as $X_C$. For each formula $A$ of $LM2$, we define the formula $A$\* of $LAF2$ in the following way :

-   - If $A=D(t_1,...,t_n)$ where $D$ is a predicate symbol or a predicate variable, then $A$\*=$A$ ;

-   - If $A=X_C(t_1,...,t_n)$, then $A$\*$=\neg X^{\ast}(t_1,...,t_n)$ ;

-   - If $A=B \f C$, then $A$\*$=B$\*$ \f C$\* ;

-   - If $A=\q xB$, then $A$\*=$\q xB$\*.

-   - If $A=\q XB$, then $A$\*=$\q XB$\*.

-   - If $A=\q X_C B$, then $A$\*=$\q X^{\ast} B$\*.

$A$\* is called the Gődel translation of $A$.

If $G$ is a classical type of $LM2$, then $\v_{LAF2} \neg \neg G$\*$ \equi G$\*.

**Proof It is easy to prove that $\v_{LAF2} G$\*$ \f \neg \neg G$\*.\
We prove $\v_{LAF2} \neg \neg 