Mathematical strength of the statement "Heyting Arithmetic admits Markov's rule"

Question

Consider the following theorem about Heyting arithmetic (HA):

For every arithmetical formula $\phi$ whose only free variable is $n$, if $\text{HA} \vdash \forall n. \phi \lor \lnot \phi$ and $\text{HA} \vdash \lnot \lnot \exists n. \phi$, then $\text{HA} \vdash \exists n. \phi$.

Or in other words, Markov's rule is admissible in Heyting arithmetic.

Proof: $\lnot \lnot \exists n. \phi$ because Heyting arithmetic is sound. By the law of excluded middle, this implies $\exists n. \phi$. Let $k$ satisfy $\phi$. Then by universal instantiation $\text{HA} \vdash \phi[n := \bar k] \lor \lnot \phi[n := \bar k]$ (where $\bar k$ is $\underbrace{1 + 1 + \dots + 1}_\text{$k$ times} + 0$). By the disjunction rule, either $\text{HA} \vdash \phi[n := \bar k]$ or $\text{HA} \vdash \lnot \phi[n := \bar k]$. The second case is impossible since Heyting arithmetic is sound. Thus $\text{HA} \vdash \phi[n := \bar k]$ which implies $\text{HA} \vdash \exists n. \phi$.
$\square$

Call this theorem T. What is the reverse mathematical strength of T? For example, is it equivalent to one of the big five?

First observation: T is weaker than Con(PA) over Peano arithmetic. Proof: Assume that Peano arithmetic proves that T implies Peano arithmetic is consistent. However, not-T also proves Peano Arithmetic is consistent because it implies there is a statement of the form $\exists n. \phi$ that Peano arithmetic can't prove. Thus Peano arithmetic proves Con(PA), which would violate Gödel's second incompletes theorem. $\square$

However, T doesn't seem entirely trivial. Since Heyting arithmetic doesn't have Markov's property, constructing the proof for $\text{HA} \vdash \exists n. \phi$ seems to require a bit of proof theory and induction.

(Note that since T is $\Pi_2^0$, it shouldn't make much of a difference whether the meta-theory is classical or constructive.)

Answer 1

$\def\ha{\mathsf{HA}}\def\down{{\downarrow}}\def\mr{\mathrel{\mathbf q}}$I believe this can be proved in a fairly weak fragment of arithmetic, such as $\mathsf{I\Delta_0+EXP}$, possibly even in a polynomial-time arithmetic ($\mathsf{PV_1}$, or $\mathsf{S^1_2}$ if you prefer) if one takes care about efficient representation of programs and such things.

The hardest part is to prove

Theorem. If $\ha\vdash\forall x\,\exists y\,\phi(x,y)$, there is a program $e$ such that $\ha\vdash\forall x\,(\{e\}(x)\down\land\phi(x,\{e\}(x)\down))$.

Proof sketch: For any formula $\phi(\vec x)$, let $n\mr\phi(\vec x)$ denote modified realizability, defined by induction on the length of the formula: $$\begin{align*} n\mr\phi&\equiv\phi,\qquad\text{if $\phi$ is atomic or $\bot$,}\\ n\mr(\phi\land\psi)&\equiv((n)_0\mr\phi)\land((n)_1\mr\psi),\\ n\mr(\phi\lor\psi)&\equiv((n)_0=0\land(n)_1\mr\phi)\lor((n)_0=1\land(n)_1\mr\psi),\\ n\mr(\phi\to\psi)&\equiv(\phi\to\psi)\land\forall m\,((m\mr\phi)\to\{n\}(m)\down\land\{n\}(m)\mr\psi),\\ n\mr\exists y\,\phi(\vec x,y)&\equiv(n)_0\mr\phi(\vec x,(n)_1),\\ n\mr\forall y\,\phi(\vec x,y)&\equiv\forall y\,(\{n\}(y)\down\land\{n\}(y)\mr\phi(\vec x,y)). \end{align*}$$ Then show by induction on the length of $\phi$ that $\ha\vdash((n\mr\phi)\to\phi)$ (easy), and show by induction on the length of a proof that if $\ha\vdash\phi(\vec x)$, then there is $e$ such that $\ha\vdash\forall\vec x\,(\{e\}(\vec x)\down\land\{e\}(\vec x)\mr\phi(\vec x))$ (tedious). Note that it is essential here that even if $\phi$ is a sentence, $e$ is not directly a numeral that realizes $\phi$, but only a program (with no input) that is supposed to output a realizer; otherwise, the whole thing would imply the existence property of $\ha$, which is not provable even in $\ha$ or $\mathsf{PA}$ itself, let alone in a much weaker theory.

Corollary. If $\ha\vdash\forall x\,(\phi(x)\lor\neg\phi(x))$, there is $e$ such that $\ha\vdash\forall x\,(\{e\}(x)\down\land(\phi(x)\leftrightarrow\{e\}(x)=0))$.

Then we can follow the argument in H. Friedman, Classically and intuitionistically provably recursive functions:

Lemma. If $\ha\vdash\phi$, then $\ha\vdash\phi^A$ for any formula $A$ (whose free variables are not quantified in $\phi$), where $\phi^A$ denotes Friedman’s translation.

Proof: Straightforward induction on the length of the proof.

Theorem. If $\ha$ proves $\forall x\,(\phi(x)\lor\neg\phi(x))$ and $\neg\neg\exists x\,\phi(x)$, then $\ha$ proves $\exists x\,\phi(x)$.

Proof: Let $e$ be such that $\ha\vdash\phi(x)\leftrightarrow\{e\}(x)=0$, whence $\ha\vdash\neg\neg\exists x\,\{e\}(x)=0$. Then $\ha\vdash(\neg\neg\exists x\,\{e\}(x)=0)^{\exists x\,\{e\}(x)=0}$, which is provably equivalent to $\exists x\,\{e\}(x)=0$ itself. Thus, $\ha\vdash\exists x\,\phi(x)$.