  ${\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.
