Duality in Intuitionistic Propositional Logic

Urzyczyn, Paweł

doi:10.4230/LIPIcs.TYPES.2020.11

File

LIPIcs.TYPES.2020.11.pdf

Filesize: 0.59 MB
10 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TYPES.2020.11
URN: urn:nbn:de:0030-drops-138901

Author Details

Paweł Urzyczyn

Institute of Informatics, University of Warsaw, Poland

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.TYPES.2020.11

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.

Subject Classification

ACM Subject Classification

Theory of computation → Proof theory
Theory of computation → Constructive mathematics
Theory of computation → Complexity theory and logic

Keywords

Intuitionistic logic
Complexity

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

Philippe de Groote. On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Information and Computation, 178(2):441-464, 2002.
Camillo Fiorentini and Mauro Ferrari. A forward unprovability calculus for intuitionistic propositional logic. In R. A. Schmidt and C. Nalon, editors, Proc. TABLEAUX 2017, volume 10501 of LNAI, pages 114-130. Springer, 2017.
D. Leivant. Assumption classes in natural deduction. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 25:1-4, 1979.
Luis Pinto and Roy Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In R. Behara, M. Fritsch and R.G. Lintz, editors, Symposia Gaussiana, Conf. A, 1993, pages 225-232. De Gruyter, 1995.
Sylvain Schmitz. Implicational relevance logic is 2-exptime-complete. J. Symb. Log., 81:641-661, 2016.
Aleksy Schubert, Wil Dekkers, and Hendrik Pieter Barendregt. Automata theoretic account of proof search. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 128-143. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
Aleksy Schubert, Paweł Urzyczyn, and Daria Walukiewicz-Chrząszcz. How hard is positive quantification? ACM Trans. Comput. Log., 17(4):30:1-30:29, 2016.
Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. Between proof construction and SAT-solving, 2021. To appear.
Tomasz Skura. Refutation systems in propositional logic. In D.M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 16, pages 115-157. Springer, 2011.
Paweł Urzyczyn. Intuitionistic games: Determinacy, completeness, and normalization. Studia Logica, 104(5):957-1001, 2016.