First, let us define the system CPRED$\omega$ of classical higher-order logic.

-   The *types* of CPRED$\omega$ are given by $${\ensuremath{{\cal T}}}\;\; ::= \;\; o \;|\; {\ensuremath{{\cal B}}}\;|\; {\ensuremath{{\cal T}}}\rightarrow {\ensuremath{{\cal T}}}$$ where ${\ensuremath{{\cal B}}}$ is a specific finite set of base types. The type $o$ is the type of propositions.

-   The set of terms of CPRED$\omega$ of type $\tau$, denoted $T_\tau$, is defined as follows:

    -   $V_\tau, \Sigma_\tau \subseteq T_\tau$,

    -   if $t_1 \in T_{\sigma\to\tau}$ and $t_2 \in T_\sigma$ then $t_1 t_2 \in T_\tau$,

    -   if $x \in V_{\tau_1}$ and $t \in T_{\tau_2}$ then $\lambda x :
            \tau_1 \,.\, t \in T_{\tau_1\to\tau_2}$,

    -   if $\varphi, \psi \in T_o$ then $\varphi \supset \psi \in
            T_o$,

    -   if $x \in V_{\tau}$ and $\varphi \in T_o$ then $\forall x :
            \tau \,.\, \varphi \in T_o$,

    where for each type $\tau$ the set $V_\tau$ is a countable set of variables and $\Sigma_\tau$ is a countable set of constants. We assume that the sets $V_\tau$ and $\Sigma_\sigma$ are all pairwise disjoint. Terms of type $o$ are *formulas*. As usual, we omit spurious brackets and assume that application associates to the left. We identify $\alpha$-equivalent terms, i.e. terms differing only in the names of bound 