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 $1 + 1 + \dots + 1 + 0$ with $1 +$ repeated $k$ times). 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.)
