recursive definitions directly, including definitions of possibly non-terminating partial functions. We believe that this feature of ${\ensuremath{{\cal I}}}_s$ makes it potentially interesting as a logic for an interactive theorem prover intended to be used for program verification.

Most popular proof assistants allow only total functions, and totality must be ensured by the user, either by very precise specifications of function domains, restricting recursion in a way that guarantees termination, explicit well-foundedness proofs, or other means.

Obviously, there is a reason why most proof assistants do not handle partial functions directly. This is to ensure consistency of the system. Combining an expressive higher-order logic with unrestricted recursion is a non-trivial problem.

There are various indirect ways of dealing with general recursion in popular theorem provers based on total logics. There are also many non-standard logics allowing partial functions directly. We discuss some related work in Sect. \[sec\_related\].

In Sect. \[sec\_I\_s\] we introduce the system ${\ensuremath{{\cal I}}}_s$. Our approach builds on the old tradition of illative combinatory logic [@illat01; @Seldin2009; @Czajka2013Accepted; @Czajka2011]. This tradition dates back to early inconsistent systems of Shönfinkel, Church and Curry proposed in the 1920s and the 1930s [@Seldin2009]. However, after the discovery of paradoxes most logicians abandoned 