DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2020.11

Duality in Intuitionistic Propositional Logic

Authors: Paweł Urzyczyn

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract

It is known that provability in propositional intuitionistic logic is Pspace-complete. As Pspace is closed under complements, there must exist a Logspace-reduction from refutability to provability. Here we describe a direct translation: given a formula φ, we define ̅φ so that ̅φ is provable if and only if φ is not.

Cite as

Paweł Urzyczyn. Duality in Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 11:1-11:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{urzyczyn:LIPIcs.TYPES.2020.11,
  author =	{Urzyczyn, Pawe{\l}},
  title =	{{Duality in Intuitionistic Propositional Logic}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{11:1--11:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.11},
  URN =		{urn:nbn:de:0030-drops-138901},
  doi =		{10.4230/LIPIcs.TYPES.2020.11},
  annote =	{Keywords: Intuitionistic logic, Complexity}
}

Search Results

Documents authored by Urzyczyn, Paweł

Duality in Intuitionistic Propositional Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message