2026-07-21T23:46:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9859 2024-03-06T10:42:24Z ddc:004 open_access

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 Markov's Principle first-order logic natural deduction Curry-Howard 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Federico Aschieri and Matteo Manighetti 2018 Is Part Of LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2016.4 urn:nbn:de:0030-drops-98590 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4 eng https://creativecommons.org/licenses/by/3.0/legalcode