I am reading the Wikipedia article about the Hilbert–Bernays provability conditions and I don't understand the following place there:
The condition that $T$ is $\omega$-consistent is generalized by the condition that if for every formula $\varphi$, if $T$ proves $\operatorname{Prov}(\sharp\varphi)$, then $T$ proves $\varphi$. Note that this indeed holds for an $\omega$-consistent $T$ because $\operatorname{Prov}(\sharp\varphi)$ means that there is a number coding for the proof of $\varphi$, and if $T$ is $\omega$-consistent then going through all natural numbers one can actually find such a particular number $a$, and then one can use $a$ to construct an actual proof of $\varphi$ in $T$.
I am trying to write the formal proof of this but one step in it remains vague to me, it is evident for me that I don't understand something important. Can anybody help me with this?
The chain of arguments that I can restore is the following. We consider a formal theory $T$ that interprets PA with the universe $U$ in the variable $x$, and we endow it with the numeration $\sharp$ of variables, terms, formulas, proofs, etc.
First, we formulate the $\omega$-consistency of $T$ as follows (I am trying to follow the definition of G.Takeuti's book , is that correct?):
for each formula $\varphi$ in $T$ in variable $x$ if the formula $$ \exists x\quad (U\ \&\ \varphi) $$ is derivable in $T$, then there exists a closed term $\tau$ in PA for which the formula $$ \neg\varphi\Big|_{x=\tau'} $$ is not derivable in $T$
($\tau'$ means the interpretation in the theory $T$ of the term $\tau$ in PA).
Second, let $\operatorname{Prf}$ be the predicate symbol that defines $\operatorname{Prov}$: $$ \operatorname{Prov}(\sharp\varphi)\quad\Leftrightarrow\quad \exists x\quad U(x)\ \&\ \operatorname{Prf}(x,\sharp\varphi) $$
Now the proof of this proposition in Wikipedia, as far as I understand it, must be the following. We assume that $\operatorname{Prov}(\sharp\varphi)$ is derivable in $T$. This leads to the following chain: $$ \text{$\exists x\ U(x)\ \&\ \operatorname{Prf}(x,\sharp\varphi)$ is derivable in $T$} $$ $$ \phantom{\text{($T$ is $\omega$-consistent)}} \qquad \Downarrow \qquad \text{($T$ is $\omega$-consistent)} $$ $$ \text{there exists a closed term $\tau$ in PA such that $\neg\operatorname{Prf}(\tau',\sharp\varphi)$ is not derivable in $T$} $$ $$ \Downarrow $$ $$ \text{there exists a closed term $\tau$ in PA such that $\operatorname{Prf}(\tau',\sharp\varphi)$ is derivable in $T$} $$ $$ \Downarrow $$ $$ \text{$\varphi$ is derivable in $T$} $$
I don't understand the second implication in this chain. Why is it true? Or if there is a mistake in these considerations, then what is the formal proof of this statement?
$\DeclareMathOperator{Prf}{Prf}$
We have some term $\tau$ such that $T \nvdash \neg \Prf(\tau, \# \phi)$.
Now in particular, all closed terms in Peano arithmetic evaluate to actual natural numbers. So WLOG, let $\tau$ be an actual natural number (or equivalently its encoding in PA) such that $T \nvdash \Prf(\tau, \# \phi)$.
Here is where we need to discuss the specific form that $\Prf$ takes. $\Prf$ is the Peano arithmetic representation of a primitive recursive predicate $P$. $P(x, y)$ is the metatheoretic predicate “$x$ is the Gödel number of a proof in $T$ of a sentence with Gödel number $y$“ in the metatheory - equivalently, we can write $P = \{(x, y) \in \mathbb{N}^2 \mid x$ is the Gödel number of a proof in $T$ of a sentence with Gödel number $y\}$. And $\Prf$, by construction, is a strong representation of $P$, meaning that $\forall x, y \in \mathbb{N} (P(x, y) \to PA \vdash \Prf(x, y))$ and $\forall x, y \in \mathbb{N} (\neg P(x, y) \to PA \vdash \neg \Prf(x, y))$.
Now either $P(\tau, \# \phi)$ or $\neg P(\tau, \# \phi)$. In the former case, we have come up with an explicit $\tau$ which encodes a proof in $T$ of $\phi$. Therefore, $T \vdash \phi$ - exactly what we wanted to show. I claim the latter case is impossible. For if $\neg P(\tau, \# \phi)$, then $PA \vdash \neg \Prf(\tau, \# \phi)$ by the fact that $\Prf$ is a strong representation of $P$. Since $T$ interprets $PA$, we know that $T \vdash \neg \Prf(\tau, \# \phi)$. But we assumed at the beginning that $T \nvdash \neg \Prf(\tau, \# \phi)$. So we have arrived at a contradiction.
Informally, we can look at $\tau$ and determine whether it actually is a proof of $\phi$. If it is not a proof of $\phi$, then we can prove within $T$ that $\tau$ is not a proof of $\phi$. This contradicts our assumption.