Completeness in Hybrid Type Theory

Areces, C.,, Blackburn, P., Huertas, A.,, and Manzano, M.. Completeness in Hybrid Type Theory. Journal of Philosophical Logic, 43(2--3):209–238, June 2014.

Download: [pdf] 

Abstract:

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 \alpha_a, where \alpha_a is an expression of any type a, as an expression of type a that rigidly returns the value that \alpha_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.

BibTeX: (download)

@ARTICLE{arec:comp13,
  author = {Areces, C., and Blackburn, P. and Huertas, A., and Manzano, M.},
  title = {Completeness in Hybrid Type Theory},
  journal = {Journal of Philosophical Logic},
  year = {2014},
  volume = {43},
  pages = {209--238},
  number = {2--3},
  month = {June},
  abstract = {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 \alpha_a,
	where \alpha_a is an expression of any type a, as an expression of
	type a that rigidly returns the value that \alpha_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.},
  owner = {areces},
  timestamp = {2013.02.10}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49