Andrews' Type Theory with Undefinedness

2014/06/29 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.7492

Abstract

\cal Q₀ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, \cal Q₀ 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}₀ is a modification of Andrews' type theory \cal Q₀ that directly formalizes the traditional approach to undefinedness. This paper presents \cal Q^{\rm u}₀ and proves that the proof system of \cal Q^{\rm u}₀ 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}₀ closely follows Andrews' development of \cal Q₀ to clearly delineate the differences between the two systems.

Related

• Simple Type Theory with Undefinedness, Quotation, and Evaluation
• An overview of type theories
• The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)
• An Equational Logical Framework for Type Theories
• Type Theory and its Meaning Explanations