In the language of arithmetic, fix a computable theory $T\supset PA^-$. Let $P_T(x)$ be the usual $\Sigma_1$ formula: for any sentence $\varphi$, $\mathbb{N}\models P_T(\ulcorner\varphi\urcorner)$ iff there is a proof of $\varphi$ from $T$.
Here are the HB conditions:
$T\supset PA^-$ satisfies HB conditions with $P_T(x)$ iff for all sentences $\varphi,\psi$,
HB1 $T\vdash \varphi$ implies $T\vdash P_T(\ulcorner\varphi\urcorner)$
HB2 $T\vdash P_T(\ulcorner\varphi\rightarrow\psi\urcorner) \rightarrow(P_T(\ulcorner\varphi\urcorner)\rightarrow P_T(\ulcorner\psi\urcorner))$
HB3 $T\vdash P_T(\ulcorner\varphi\urcorner)\rightarrow P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$
I found some sources where it says any computable $T$ extending $PA^-$ with $P_T(x)$ satisfies HB1 and HB2. My concern is that all things I searched so far only says that any computable theory extending PA satisfies HB3 with this $P_T(x)$, instead of any computable theory extending $PA^-$. But in my thinking, HB3 should still be satisfied for any computable theory extending $PA^-$, so I am wondering if I am right.
Fix a comptuable $T\supset PA^-$ and fix a sentence $\varphi$. Then I think $T\vdash P_T(\ulcorner\varphi\urcorner) \rightarrow P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$. It suffices to show that $T\models P_T(\ulcorner\varphi\urcorner) \rightarrow P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$. Since $P_T(\ulcorner\varphi\urcorner) \rightarrow P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$ is still a $\Sigma_1$ sentence for a fixed $\ulcorner \varphi\urcorner$ as we can write numbers by using $1+\cdots+1$, it suffices to show that $\mathbb{N}\models P_T(\ulcorner\varphi\urcorner) \rightarrow P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$ because $\Sigma_1$ sentences go upwards. And this is clear from HB1: if $\mathbb{N}\models P_T(\ulcorner\varphi\urcorner)$, then $T\vdash \varphi$, so $T\vdash P_T(\ulcorner\varphi\urcorner)$, so $\mathbb{N}\models P_T(\ulcorner P_T(\ulcorner\varphi\urcorner)\urcorner)$.
Am I missing something, or am I correct?