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

Aschieri, Federico; Manighetti, Matteo

doi:10.4230/LIPIcs.TYPES.2016.4

File

LIPIcs.TYPES.2016.4.pdf

Filesize: 0.57 MB
17 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TYPES.2016.4
URN: urn:nbn:de:0030-drops-98590

Author Details

Federico Aschieri

Matteo Manighetti

Cite AsGet 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

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.

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

References

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.
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.
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.
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.
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.
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.
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.
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.
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.
Matteo Manighetti. Computational interpretations of markov’s principle. Master’s thesis, Wien, Techn. Univ., Wien, 2016. URL: https://arxiv.org/abs/1611.03714.
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.
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.
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.