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

TL;DR

This paper establishes a Curry-Howard correspondence for a logic extended with Markov's principle, simplifies existing proofs, and provides a computational interpretation for arithmetic with Markov's principle.

Contribution

It offers a simpler proof of the Curry-Howard correspondence for Herbrand constructive logics and extends it to unrestricted Markov's principle, with applications to arithmetic.

Findings

Proof terms for existential formulas reduce to witness lists

The logic is Herbrand constructive, proving existential formulas with Herbrand disjunctions

Provides a new computational interpretation of arithmetic with Markov's principle

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.