x.(x \, x)$ is typable but is not strongly normalizing. With the equation $X=X\f X$, every term can be typed. By making some natural assumptions on the recursive equations the strong normalization can be preserved. The simplest condition is to accept the equation $X = F$ (where $F$ is a type containing the variable $X$) only when the variable $X$ is positive in $F$. For a set $\{X_i = F_i \;/ \; i \in I\}$ of mutually recursive equations, Mendler [@Mend1] has given a very simple and natural condition that ensures the strong normalization of the system. He also showed that the given condition is necessary to have the strong normalization.

Mendler’s result concerns the implicative fragment of intuitionistic logic. We extend here his result to full classical logic. We now assume ${\cal A}$ contains a specified subset ${\cal X}=\{X_i \; / \; i \in I \}$.

\[positive\] Let $X \in {\cal X}$. We define the subsets ${\cal P}^+(X)$ and ${\cal P}^-(X)$ of ${\cal T}$ (resp. ${\cal T}'$ ) as follows.

-   $X \in {\cal P}^+(X)$

-   If $A \in ({\cal X}- \{X\})\cup \cal{A}$, then $A \in {\cal
    P}^+(X) \cap {\cal P}^-(X)$.

-   If $A \in {\cal P}^-(X)$ and $B 