On the philosophy and mathematics of hybrid partial type theory

Abstract

The aim of this paper is to present the philosophical influences and motivations of Hybrid Partial Type Theory (HPTT), a partial type theory combined with a strong version of hybrid logic in which the concepts of existence and denotation emerge naturally. The text is divided into three main parts. Firstly, we present and discuss some formal systems dealing with existence and denotation in both first-order logic and type theory. Then, we move to the framework of modal logic, introducing the distinction between constant and varying domains, as well as the hybrid machinery. Finally, we give a succinct account of the semantics of HPTT and provide new definitions of existence and denotation within the system, together with a reflection on de dicto and de re statements and some validities sharing an explicit philosophical characterization.