Andrews' Type Theory with Undefinedness

TL;DR

This paper introduces ${ m Q}_0^{ m u}$, a modification of Andrews' type theory that formalizes the traditional approach to undefined terms, and proves its soundness and completeness.

Contribution

It presents ${ m Q}_0^{ m u}$, a new type theory formalizing undefinedness, with proven soundness and completeness, extending Andrews' ${ m Q}_0$.

Findings

${ m Q}_0^{ m u}$ is sound and complete.

The development closely follows Andrews' ${ m Q}_0$.

Formalizes the traditional approach to undefinedness.

Abstract

${\cal Q}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${\cal Q}_0$ does not admit undefined terms. The "traditional approach to undefinedness" in mathematical practice is to treat undefined terms as legitimate, nondenoting terms that can be components of meaningful statements. ${\cal Q}^{\rm u}_{0}$ is a modification of Andrews' type theory ${\cal Q}_0$ that directly formalizes the traditional approach to undefinedness. This paper presents ${\cal Q}^{\rm u}_{0}$ and proves that the proof system of ${\cal Q}^{\rm u}_{0}$ is sound and complete with respect to its semantics which is based on Henkin-style general models. The paper's development of ${\cal Q}^{\rm u}_{0}$ closely follows Andrews' development of ${\cal Q}_0$ to clearly delineate the differences between the two systems.