Hybrid Partial Type Theory
Loading...
Official URL
Full text at PDC
Publication date
2023
Advisors (or tutors)
Editors
Journal Title
Journal ISSN
Volume Title
Publisher
Cambridge University Press
Citation
MANZANO M, HUERTAS A, BLACKBURN P, MARTINS M, ARANDA V. HYBRID PARTIAL TYPE THEORY. The Journal of Symbolic Logic. Published online 2023:1-43. doi:10.1017/jsl.2023.33
Abstract
In this article we define a logical system called Hybrid Partial Type Theory (HPTT ). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to particular worlds. We motivate this combination of ideas in the introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for HPTT .