---
abstract: 'We present an illative system ${\ensuremath{{\cal I}}}_s$ of classical higher-order logic with subtyping and basic inductive types. The system ${\ensuremath{{\cal I}}}_s$ allows for direct definitions of partial and general recursive functions, and provides means for handling functions whose termination has not been proven. We give examples of how properties of some recursive functions may be established in our system. In a technical appendix to the paper we prove consistency of ${\ensuremath{{\cal I}}}_s$. The proof is by model construction. We then use this construction to show conservativity of ${\ensuremath{{\cal I}}}_s$ over classical first-order logic. Conservativity over higher-order logic is conjectured, but not proven.'
author:
- Łukasz Czajka
bibliography:
- 'biblio.bib'
title: 'Partiality and Recursion in Higher-Order Logic'
---

[**Note:**]{} This paper is an extended technical report based on a conference paper with the same title published by Springer-Verlag in the proceedings of FoSSaCS 2013. The final publication is available at .

Table of Contents {#table-of-contents .unnumbered}
=================

starttoc[toc]{}

Introduction
============

We present an illative $\lambda$-calculus system ${\ensuremath{{\cal I}}}_s$ of classical higher-order logic with subtyping and basic inductive types. Being illative means that the system is a combination of higher-order logic with the *untyped* $\lambda$-calculus. It therefore allows for unrestricted 