Completeness in Hybrid Type Theory

Journal of Philosophical Logic 43 (2-3):209-238 (2014)
  Copy   BIBTEX

Abstract

We show that basic hybridization makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i$\end{document} in propositional and first-order hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha _a$\end{document} is an expression of any type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document}, as an expression of type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document} that rigidly returns the value that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha_a$\end{document} receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Hybrid Type Theory: A Quartet in Four Movements.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2011 - Principia: An International Journal of Epistemology 15 (2):225.
Completeness: from Gödel to Henkin.Maria Manzano & Enrique Alonso - 2014 - History and Philosophy of Logic 35 (1):1-26.
Hybrid Identities and Hybrid Equational Logic.Klaus Denecke - 1995 - Mathematical Logic Quarterly 41 (2):190-196.
Remarks on Gregory's “actually” operator.Patrick Blackburn & Maarten Marx - 2002 - Journal of Philosophical Logic 31 (3):281-288.
Meeting Strength in Substructural Logics.Yde Venema - 1995 - Studia Logica 54 (1):3-32.
Hybrid logics with Sahlqvist axioms.Balder Cate, Maarten Marx & Petrúcio Viana - 2005 - Logic Journal of the IGPL 13 (3):293-300.
Special Issue on Hybrid Logics.Carlos Areces & Patrick Blackburn - 2010 - Journal of Applied Logic 8 (4):303-304.
Hybrid completeness.P. Blackburn & M. Tzakova - 1998 - Logic Journal of the IGPL 6 (4):625-650.
Hybrid counterfactual logics David Lewis meets Arthur prior again.Katsuhiko Sano - 2009 - Journal of Logic, Language and Information 18 (4):515-539.
Remarks on Gregory's “Actually” Operator.Blackburn Patrick & Marx Maarten - 2002 - Journal of Philosophical Logic 31 (3):281-288.

Analytics

Added to PP
2017-06-22

Downloads
23 (#584,438)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

María Manzano
Universidad de Salamanca
Patrick Blackburn
Roskilde University

References found in this work

Generalized quantifiers and natural language.John Barwise & Robin Cooper - 1981 - Linguistics and Philosophy 4 (2):159--219.
The Proper Treatment of Quantification in Ordinary English.Richard Montague - 1974 - In Richmond H. Thomason (ed.), Formal Philosophy. Yale University Press.
Generalized Quantifiers and Natural Language.Jon Barwise - 1980 - Linguistics and Philosophy 4:159.
A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Completeness in the theory of types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.

View all 28 references / Add more references