Artículo
Completeness in Hybrid Type Theory
Fecha de publicación:
05/2014
Editorial:
Springer
Revista:
Journal of Philosophical Logic
ISSN:
0022-3611
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
We show that basic hybridization (adding nominals and @ operators) 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 @i@i in propositional and first-order hybrid logic. This means: interpret @iαa@iαa , where αaαa is an expression of any type aa , as an expression of type aa that rigidly returns the value that αaαa receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) 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.
Palabras clave:
Hybrid Logic
,
Type Theory
,
Higher-Order Modal Logic
,
Nominals
,
@ Operators
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CCT - CORDOBA)
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Citación
Areces, Carlos Eduardo; Blackburn, Patrick; Huertas, Antonia; Manzano, Maria; Completeness in Hybrid Type Theory; Springer; Journal of Philosophical Logic; 43; 2-3; 5-2014; 209-238
Compartir
Altmétricas