${ \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.
Categories: math.LO cs.LO