Document Open Access Logo

Duality in Intuitionistic Propositional Logic

Author Paweł Urzyczyn

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.11.pdf
  • Filesize: 0.59 MB
  • 10 pages

Document Identifiers

Author Details

Paweł Urzyczyn
  • Institute of Informatics, University of Warsaw, Poland

Cite As Get 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

  1. Philippe de Groote. On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Information and Computation, 178(2):441-464, 2002. Google Scholar
  2. 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. Google Scholar
  3. D. Leivant. Assumption classes in natural deduction. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 25:1-4, 1979. Google Scholar
  4. 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. Google Scholar
  5. Sylvain Schmitz. Implicational relevance logic is 2-exptime-complete. J. Symb. Log., 81:641-661, 2016. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. Between proof construction and SAT-solving, 2021. To appear. Google Scholar
  9. 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. Google Scholar
  10. Paweł Urzyczyn. Intuitionistic games: Determinacy, completeness, and normalization. Studia Logica, 104(5):957-1001, 2016. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact