a consistency proof.

In Sect. \[sec\_partiality\] we provide examples of proofs in ${\ensuremath{{\cal I}}}_s$ indicating possible applications of our approach to the problem of dealing with partiality, non-termination and general recursion in higher-order logic. We are mainly interested in partiality arising from non-termination of non-well-founded recursive definitions.

For lack of space we omit proofs of most of the lemmas and theorems we state. The proofs of non-trivial results may be found in technical appendices to this paper.

The Illative System {#sec_I_s}
===================

In this section we present the system ${\ensuremath{{\cal I}}}_s$ of illative classical higher-order logic with subtyping and derive some of its basic properties.

\[def\_I\_s\]

The system ${\ensuremath{{\cal I}}}_s$ consists of the following.

-   A countably infinite set of variables $V_s = \{x, y, z, \ldots
        \}$ and a set of constants $\Sigma_{s}$.

-   The set of sorts ${\ensuremath{{\cal S}}}= \{{\ensuremath{\mathrm{Type}}}, {\ensuremath{\mathrm{Prop}}}\}$.

-   The set of *basic inductive types* ${\ensuremath{{\cal T}}}_I$ is defined inductively by the rule: if $\iota_{1,1},\ldots,\iota_{1,n_1},\ldots,\iota_{m,1},\ldots,\iota_{m,n_m}
        \in {\ensuremath{{\cal T}}}_I \cup \{\star\}$ then $$\mu(\langle \iota_{1,1},\ldots,\iota_{1,n_1} \rangle, \ldots,
        \langle \iota_{m,1},\ldots,\iota_{m,n_m} \rangle) \in {\ensuremath{{\cal T}}}_I$$ where $m \in {\ensuremath{\mathbb{N}}}_+$ and $n_1,\ldots,n_m \in {\ensuremath{\mathbb{N}}}$.

-   We define the sets of *constructors* ${\ensuremath{{\cal C}}}$, *destructors* ${\ensuremath{{\cal D}}}$, and *tests* ${\ensuremath{{\cal O}}}$ 