Simple Type Theory with Undefinedness, Quotation, and Evaluation

William M. Farmer

2014 (revised 2016)

Abstract

This paper presents a version of simple type theory called Q0uqe that
is based on Q0, the elegant formulation of Church's type theory
created and extensively studied by Peter B. Andrews.  Q0uqe directly
formalizes the traditional approach to undefinedness in which
undefined expressions are treated as legitimate, nondenoting
expressions that can be components of meaningful statements.  Q0uqe is
also equipped with a facility for reasoning about the syntax of
expressions based on quotation and evaluation.  Quotation is used to
refer to a syntactic value that represents the syntactic structure of
an expression, and evaluation is used to refer to the value of the
expression that a syntactic value represents.  With quotation and
evaluation it is possible to reason in Q0uqe about the interplay of
the syntax and semantics of expressions and, as a result, to formalize
in Q0uqe syntax-based mathematical algorithms. The paper gives the
syntax and semantics of Q0uqe as well as a proof system for Q0uqe.
The proof system is shown to be sound for all formulas and complete
for formulas that do not contain evaluations. The paper also
illustrates some applications of Q0uqe.

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