variables are considered identical.

-   The system CPRED$\omega$ is given by the following rules and axioms, where $\Delta$ is a finite set of formulas, $\varphi, \psi$ are formulas. The notation $\Delta, \varphi$ is a shorthand for $\Delta \cup \{\varphi\}$.

    [**Axioms**]{}

    -   $\Delta, \varphi {\ensuremath{\vdash}}\varphi$

    -   $\Delta {\ensuremath{\vdash}}\forall p : o \,.\, ((p \supset \bot) \supset
            \bot) \supset p$ where $\bot \equiv \forall p : o \,.\, p$

    [**Rules**]{}

    [lr]{} $
          {\supset_i^P:}\; \inferrule{\Delta, \varphi {\ensuremath{\vdash}}\psi}{\Delta {\ensuremath{\vdash}}\varphi \supset \psi}
        $ & $
          {\supset_e^P:}\; \inferrule{\Delta {\ensuremath{\vdash}}\varphi \supset
            \psi \;\;\; \Delta {\ensuremath{\vdash}}\varphi}{\Delta {\ensuremath{\vdash}}\psi}
        $\
    &\
    $
          {\forall_i^P:}\; \inferrule{\Delta {\ensuremath{\vdash}}\varphi}{\Delta {\ensuremath{\vdash}}\forall x : \tau \,.\, \varphi} \; x
          \notin FV(\Delta), x \in V_\tau
        $ & $
          {\forall_e^P:}\; \inferrule{\Delta {\ensuremath{\vdash}}\forall x : \tau \,.\, \varphi}{\Delta
            {\ensuremath{\vdash}}\varphi[x/t]}\; t \in T_\tau
        $\
    &\

In CPRED$\omega$, we define Leibniz equality in type $\tau \in {\ensuremath{{\cal T}}}$ by $$t_1 =_\tau t_2 \equiv \forall p : \tau \to o \,.\, p t_1 \supset p t_2$$ The system CPRED$\omega$ is intensional. An extensional variant E-CPRED$\omega$ may be obtained by adding the following axioms for all $\tau, \sigma \in {\ensuremath{{\cal T}}}$: $$e_f^P: \forall f_1, f_2 : \tau \to \sigma \,.\, \left(\forall x : \tau
\,.\, f_1 x =_\sigma f_2 x \right) \supset (f_1 