this approach. A notable exception was Haskell Curry and his school, but not much progress was made in establishing consistency of illative systems strong enough to interpret traditional logic. Only in the 1990s some first-order illative systems were shown consistent and complete for traditional first-order logic [@illat01; @illat02]. The system ${\ensuremath{{\cal I}}}_s$, in terms of the features it provides, may be considered an extension of the illative system ${\ensuremath{{\cal I}}}_\omega$ from [@Czajka2013Accepted]. We briefly discuss the relationship between ${\ensuremath{{\cal I}}}_s$ and ${\ensuremath{{\cal I}}}_\omega$ in Sect. \[sec\_related\].

Because ${\ensuremath{{\cal I}}}_s$ is based on the untyped $\lambda$-calculus, its consistency is obviously open to doubt. In an appendix we give a proof by model construction of consistency of ${\ensuremath{{\cal I}}}_s$. Unfortunately, the proof is too long to fit within the page limits of a conference paper. In Sect. \[sec\_consistent\] we give a general overview of the proof. The model construction is similar to the one from [@Czajka2013Accepted] for the traditional illative system ${\ensuremath{{\cal I}}}_\omega$. It is extended and adapted in a non-trivial way to account for additional features of ${\ensuremath{{\cal I}}}_s$. To our knowlege ${\ensuremath{{\cal I}}}_s$ is the first higher-order illative system featuring subtypes and some form of induction, for which there is 