Is there a theory between HA and PA that doesn't have Markov's rule?

Question

A theory $T$ admits Markov's rule when

For every formula $\phi(n)$, if $$T \vdash \forall n \in \mathbb N. \phi(n) \lor \lnot \phi(n)$$ and $$T \vdash \lnot \lnot \exists n \in \mathbb N. \phi(n)$$ then $$T \vdash \exists n \in \mathbb N. \phi(n)$$

Heyting arithmetic (HA) and Peano arithmetic (PA) both satisfy this, but for very different reasons.

HA admits Markov's rule because it is sound and it has the disjunction property.

Proof: If there is a $n$ such that $\phi(n)$, then HA doesn't prove $\lnot \phi(n)$ (by soundness) and thus proves $\phi(n)$ instead (by the disjunction property). If not, this means $\lnot \exists n. \phi(n)$, but this is impossible because $HA \vdash \lnot \lnot \exists n. \phi(n)$ and HA is sound.
$\square$

(Note that the meta-theory of this proof is classical, but since the statement "$T$ admits Markov's rule" is $\Pi^0_2$, there is also a constructive proof because of the Friedman translation.)

$PA$ admits Markov's rule because $PA$ proves Markov's principle.

Since these reasons are so different, it's not clear that this property applies to every theory in between them. My question: is there a recursively enumerable theory T (such that $HA \subset T \subset PA$) that doesn't admit Markov's rule?

Answer 1

$\def\prf{\mathrm{Prf}}\def\pr{\mathrm{Pr}}\def\con{\mathrm{Con}}\def\f{\ulcorner\bot\urcorner}\def\ha{\mathsf{HA}}$Let $\prf(x,y)$ be the formalized proof predicate for either HA or PA (it doesn’t matter), and $$\begin{align*} \pr(y)&\equiv\exists x\,\prf(x,y),\\ \con&\equiv\neg\pr(\f),\\ T&=\ha+\con\lor\neg\con,\\ \phi(x)&\equiv\con\lor\prf(x,\f). \end{align*}$$ Clearly $\ha\subseteq T\subseteq\mathsf{PA}$. We have $$T\vdash\forall x\,(\phi(x)\lor\neg\phi(x))$$ as assuming either $\con$ or $\neg\con$, $\phi(x)$ reduces to the decidable formula $\prf(x,\f)$. Since $\exists$ distributes over $\lor$, $$T\vdash\exists x\,\phi(x)\equiv\con\lor\pr(\f).$$ This is an instance of excluded middle, hence $$T\vdash\neg\neg\exists x\,\phi(x).$$ However, $$T\nvdash\exists x\,\phi(x):$$ if we assume for contradiction $\exists x\,\phi(x)$ is provable in $T$, then it is in particular provable in $\ha+\neg\con$, thus $$\ha\vdash\neg\con\to\pr(\f).$$ Using the numerical existence property for negative extensions of HA, there is $n\in\mathbb N$ such that $$\ha\vdash\neg\con\to\prf(\overline n,\f).$$ However, HA/PA is consistent, hence $n$ is not actually a code of a proof of $\bot$. Thus the decidable sentence $\prf(\overline n,\f)$ is false, and therefore refutable in HA. It follows that $$\ha\vdash\con,$$ contradicting Gödel’s theorem.

(The argument above does not rely on any particularly specific properties of $\con$; any true but PA-unprovable $\Pi_1$ sentence would work.)