order variables denoted by $X_C,Y_C,Z_C$...., and called classical variables.\
Let $X$ be an $n$-ary predicate variable or predicate symbol. A type $A$ is said to be ending with $X$ if and only if $A$ is obtained by the following rules :

-   - $X(t_1,...,t_n)$ ends with $X$;

-   - If $B$ ends with $X$, then $A \f B$ ends with $X$ for every type $A$ ;

-   - If $A$ ends with $X$, then $\q vA$ ends with $X$ for every variable $v$.\

A type $A$ is said to be a classical type if and only if $A$ ends with $\perp$ or a classical variable.\
We add to the $AF2$ type system the new following rules :

-   (0$'$) $\G\v C : \q X_C \{ \neg \neg X_C \f X_C \}$

-   (6$'$) If $\G\v t:A$, and $X_C$ has no free occurence in $\G$, then $\G\v t: \q
    X_C A$.

-   (7$'$) If $\G\v t: \q X_C A$, and $G$ is a classical type, then $\G\v t:A[G/ X_C]$.

We call $M2$ the new type system, and we write $\G \v_{M2} t:A$ if $t$ is of type $A$ in the context $\G$.\
We extend the definition of $\lhd$ by : $\q 