Document Open Access Logo

On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic

Authors Federico Aschieri, Matteo Manighetti

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2016.4.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Markov's Principle
  • first-order logic
  • natural deduction
  • Curry-Howard

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possible witnesses. As corollary, we derive that the logic is Herbrand constructive: whenever it proves any existential formula, it proves also an Herbrand disjunction for the formula. Finally, using the techniques just introduced, we also provide a new computational interpretation of Arithmetic with Markov's principle.

Cite As Get BibTex

Federico Aschieri and Matteo Manighetti. On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.4

Author Details

Federico Aschieri
Matteo Manighetti

References

  1. Federico Aschieri. Strong normalization for HA + EM1 by non-deterministic choice. In Proceedings First Workshop on Control Operators and their Semantics, COS 2013, Eindhoven, The Netherlands, June 24-25, 2013., pages 1-14, 2013. URL: http://dx.doi.org/10.4204/EPTCS.127.1.
  2. Federico Aschieri, Stefano Berardi, and Giovanni Birolo. Realizability and strong normalization for a Curry-Howard interpretation of ha+em1. In Computer science logic 2013, volume 23 of LIPIcs. Leibniz Int. Proc. Inform., pages 45-60. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2013. Google Scholar
  3. Federico Aschieri and Margherita Zorzi. A "game semantical" intuitionistic realizability validating Markov’s principle. In 19th International Conference on Types for Proofs and Programs, volume 26 of LIPIcs. Leibniz Int. Proc. Inform., pages 24-44. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2014. Google Scholar
  4. Federico Aschieri and Margherita Zorzi. On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand’s theorem. Theoret. Comput. Sci., 625:125-146, 2016. URL: http://dx.doi.org/10.1016/j.tcs.2016.02.028.
  5. Samuel R. Buss. On Herbrand’s theorem. In Logic and computational complexity (Indianapolis, IN, 1994), volume 960 of Lecture Notes in Comput. Sci., pages 195-209. Springer, Berlin, 1995. URL: http://dx.doi.org/10.1007/3-540-60178-3_85.
  6. Ph. de Groote, editor. The Curry-Howard isomorphism, volume 8 of Cahiers du Centre de Logique [Reports of the Center of Logic]. Academia-Erasme, Louvain-la-Neuve; Université Catholique de Louvain, Département de Philosophie, Louvain-la-Neuve, 1995. Google Scholar
  7. Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280-287, 1958. URL: http://dx.doi.org/10.1111/j.1746-8361.1958.tb01464.x.
  8. Hugo Herbelin. An intuitionistic logic that proves Markov’s principle. In 25th Annual IEEE Symposium on Logic in Computer Science LICS 2010, pages 50-56. IEEE Computer Soc., Los Alamitos, CA, 2010. Google Scholar
  9. S. C. Kleene. On the interpretation of intuitionistic number theory. J. Symbolic Logic, 10:109-124, 1945. URL: http://dx.doi.org/10.2307/2269016.
  10. Matteo Manighetti. Computational interpretations of markov’s principle. Master’s thesis, Wien, Techn. Univ., Wien, 2016. URL: https://arxiv.org/abs/1611.03714.
  11. Dag Prawitz. Ideas and results in proof theory. In Proceedings of the Second Scandinavian Logic Symposium (Univ. Oslo, Oslo, 1970), pages 235-307. Studies in Logic and the Foundations of Mathematics, Vol. 63. North-Holland, Amsterdam, 1971. Google Scholar
  12. A. S. Troelstra. Corrections and additions to: Metamathematical investigation of intuitionistic arithmetic and analysis (Lecture Notes in Math., Vol. 344, Springer, Berlin, 1973). Mathematisch Intituut, Universiteit van Amsterdam, Amsterdam, 1974. Report 74-16. Google Scholar
  13. A. S. Troelstra and D. van Dalen. Constructivism in mathematics. Vol. I, volume 121 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. An introduction. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact