Completeness in hybrid type theory

Mostrar todas las versiones(2)

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 w...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Areces, Carlos Eduardo, Blackburn, Patrick, Huertas, Antonia, Manzano, María
Formato: article
Lenguaje:Inglés
Publicado: 2021
Materias:
Hybrid logic
Type theory
Higher-order modal logic
Nominals
@ operators
Acceso en línea:http://hdl.handle.net/11086/20021
https://doi.org/10.1007/s10992-012-9260-4
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R14111086-20021
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Hybrid logic
Type theory
Higher-order modal logic
Nominals
@ operators
spellingShingle Hybrid logic
Type theory
Higher-order modal logic
Nominals
@ operators
Areces, Carlos Eduardo
Blackburn, Patrick
Huertas, Antonia
Manzano, María
Completeness in hybrid type theory
topic_facet Hybrid logic
Type theory
Higher-order modal logic
Nominals
@ operators
description 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 in propositional and first-order hybrid logic. This means: interpret @iαa, where αa is an expression of any type a, as an expression of type a that rigidly returns the value that α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 in hybrid 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 logic over Henkin’s logic.
format article
author Areces, Carlos Eduardo
Blackburn, Patrick
Huertas, Antonia
Manzano, María
author_facet Areces, Carlos Eduardo
Blackburn, Patrick
Huertas, Antonia
Manzano, María
author_sort Areces, Carlos Eduardo
title Completeness in hybrid type theory
title_short Completeness in hybrid type theory
title_full Completeness in hybrid type theory
title_fullStr Completeness in hybrid type theory
title_full_unstemmed Completeness in hybrid type theory
title_sort completeness in hybrid type theory
publishDate 2021
url http://hdl.handle.net/11086/20021
https://doi.org/10.1007/s10992-012-9260-4
work_keys_str_mv AT arecescarloseduardo completenessinhybridtypetheory
AT blackburnpatrick completenessinhybridtypetheory
AT huertasantonia completenessinhybridtypetheory
AT manzanomaria completenessinhybridtypetheory
bdutipo_str Repositorios
_version_ 1764820394874765313

Ejemplares similares