2014/06/25 by Farmer, William M.
#03B15 (Primary) #03B35 (Secondary) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1406.6706
This paper presents a version of simple type theory called \cal Q\rm uqe0 that is based on \cal Q0, the elegant formulation of Church's type theory created and extensively studied by Peter B. Andrews. \cal Q\rm uqe0 directly formalizes the traditional approach to undefinedness in which undefined expressions are treated as legitimate, nondenoting expressions that can be components of meaningful statements. \cal Q\rm uqe0 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 \cal Q\rm uqe0 about the interplay of the syntax and semantics of expressions and, as a result, to formalize in \cal Q\rm uqe0 syntax-based mathematical algorithms. The paper gives the syntax and semantics of \cal Q\rm uqe0 as well as a proof system for \cal Q\rm uqe0. 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 \cal Q\rm uqe0.