$\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.