1 Search Results for "Litak, Tadeusz"

Document

DOI: 10.4230/LIPIcs.FSCD.2017.27

Negative Translations and Normal Modality

Authors: Tadeusz Litak, Miriam Polzer, and Ulrich Rabenstein

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

We discuss the behaviour of variants of the standard negative translations - Kolmogorov, Gödel-Gentzen, Kuroda and Glivenko - in propositional logics with a unary normal modality. More specifically, we address the question whether negative translations as a rule embed faithfully a classical modal logic into its intuitionistic counterpart. As it turns out, even the Kolmogorov translation can go wrong with rather natural modal principles. Nevertheless, we isolate sufficient syntactic criteria ensuring adequacy of well-behaved (or, in our terminology, regular) translations for logics axiomatized with formulas satisfying these criteria, which we call enveloped implications. Furthermore, a large class of computationally relevant modal logics - namely, logics of type inhabitation for applicative functors (a.k.a. idioms) - turns out to validate the modal counterpart of the Double Negation Shift, thus ensuring adequacy of even the Glivenko translation. All our positive results are proved purely syntactically, using the minimal natural deduction system of Bellin, de Paiva and Ritter extended with additional axioms/combinators and hence also allow a direct formalization in a proof assistant (in our case Coq).

Cite as

Tadeusz Litak, Miriam Polzer, and Ulrich Rabenstein. Negative Translations and Normal Modality. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{litak_et_al:LIPIcs.FSCD.2017.27,
  author =	{Litak, Tadeusz and Polzer, Miriam and Rabenstein, Ulrich},
  title =	{{Negative Translations and Normal Modality}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.27},
  URN =		{urn:nbn:de:0030-drops-77412},
  doi =		{10.4230/LIPIcs.FSCD.2017.27},
  annote =	{Keywords: negative translations, intuitionistic modal logic, normal modality, double negation}
}

Refine by Author
1 Litak, Tadeusz
1 Polzer, Miriam
1 Rabenstein, Ulrich

Refine by Classification

Refine by Keyword
1 double negation
1 intuitionistic modal logic
1 negative translations
1 normal modality

Refine by Type
1 document

Refine by Publication Year
1 2017

1 Search Results for "Litak, Tadeusz"

Negative Translations and Normal Modality

Abstract

Cite as

Thanks for your feedback!

Could not send message