Partiality and Recursion in Higher-order Logic

TL;DR

This paper introduces an illative system for classical higher-order logic that supports partial and recursive functions, providing a framework for reasoning about functions with unproven termination and establishing their properties.

Contribution

The paper presents a new illative system I_s for higher-order logic that allows direct definitions of partial and recursive functions, along with a proof of its consistency.

Findings

Proves the consistency of the I_s system via model construction.

Demonstrates how properties of recursive functions can be established within I_s.

Shows conservativity of I_s over classical first-order logic.

Abstract

We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system 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 I_s. The proof is by model construction. We then use this construction to show conservativity of I_s over classical first-order logic. Conservativity over higher-order logic is conjectured, but not proven.