Andrews's Type System with Undefinedness

William M. Farmer

2008 (revised 2014)

Abstract

Q0 is an elegant version of Church's type theory formulated and
extensively studied by Peter B. Andrews.  Like other traditional
logics, Q0 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.  Q0u is a modification of Andrews' type theory Q0 that
directly formalizes the traditional approach to undefinedness.  This
paper presents Q0u and proves that the proof system of Q0u is sound
and complete with respect to its semantics which is based on
Henkin-style general models.  The paper's development of Q0u closely
follows Andrews' development of Q0 to clearly delineate the
differences between the two systems.

Note: Q0 stands for ${\cal Q}_0$ and Q0u stands for ${\cal Q}^{\rm
u}_{0}$ in TeX.