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.
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2016.4, author = {Aschieri, Federico and Manighetti, Matteo}, title = {{On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {4:1--4:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4}, URN = {urn:nbn:de:0030-drops-98590}, doi = {10.4230/LIPIcs.TYPES.2016.4}, annote = {Keywords: Markov's Principle, first-order logic, natural deduction, Curry-Howard} }
Feedback for Dagstuhl Publishing