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.