If $T$ is a consistent theory of arithmetic able to represent all computable functions, and in particular the $Proof(y,x)$ relation on natural numbers where $y$ is an encoding of a proof terminating in the formula with number $x$. I.e. if the relation holds on numbers $m,n$ then $T\vdash Proof(\underline{m},\underline{n})$ and otherwise $T\vdash \neg Proof(\underline{m},\underline{n})$. Ambiguity about the distinction between the relation and the formula for the relation is permitted. Suppose in $T$ the $Neg(y,x)$ relation, where $x$ is the number of the formula which is the negation of the formula for $y$. Moreover suppose for every formula $\varphi$,
$$T\vdash Neg(\varphi,v)\leftrightarrow v = \ulcorner\neg\varphi\urcorner$$ $$T\vdash Neg(v,\varphi)\rightarrow v<\ulcorner\varphi\urcorner$$
I take it this implies that we can universally generalize these formulae.
If we further define $Proof^{**}(y,x)$ as
$$Proof(y,x)\land \forall z<y\forall v([Neg(v,x)\lor Neg(x,v)]\rightarrow \neg Proof(z,x)$$
I have just shown that $T\vdash Proof^{**}(\underline{n},\ulcorner\varphi\urcorner)\leftrightarrow Proof(\underline{n},\ulcorner\varphi\urcorner)$. If we next define $Prv^{**}(x)$ as $\exists y Proof^{**}(y,x)$ then I need to prove
$$T\vdash Prv^{**}(\ulcorner\varphi\urcorner)\rightarrow \neg Prv^{**}(\ulcorner\neg\varphi\urcorner)$$
If $\varphi$ has proof coded $n$ then by consistency it doesn't have a proof of $\neg\varphi$ and by representability, $T\vdash \neg Proof^{**}(\underline{0},\ulcorner\neg\varphi\urcorner)\land ...\land \neg Proof^{**}(\underline{n-1},\neg\varphi) $ from which the provability follows. If $\varphi$ doesn't have a proof, though, I think what I should be trying to do is show $T\vdash \neg Prv^{**}(\ulcorner \varphi\urcorner)$ but this is equivalent to proving an unbounded universally quantified sentence, and I'm not sure how that could be possible. On the other hand we know that there are some sentences neither provable nor disprovable, so if $\varphi$ is one such sentence then showing this might be impossible. Perhaps somehow I still need to show the conditional without necessarily showing any one part of it? ... But I'm quite lost about how that might go.
For simplicity, let's conflate objects and their codes (obviously this isn't allowed when writing the proof, but it can be useful for coming up with the proof). Intuitively, $Prv^{**}(p)$ says "there is a proof of $p$ shorter than any disproof of $p$." I don't quite mean "shorter," of course, but rather "of smaller Goedel number," but that's a bit of a mouthful. So (reasoning in $T$) suppose for a contradiction that the statement "$Prv^{**}(p)\wedge Prv^{**}(\neg p)$" held. Then there is a proof $a$ of $p$ with no shorter disproof of $p$, but also a disproof $b$ of $p$ with no shorter proof of $p$. OK - is $a<b$ or is $b<a$?