= Solution
Write $BA=P(\ulcorner A\urcorner)$, with the corner notation understood as the numeral for the <Gödel number>. An <arithmetical provability predicate> numerates the theorems of $S$ in the standard natural numbers and satisfies the <Hilbert-Bernays-Löb derivability conditions>:
$$
\begin{aligned}
& S\vdash A\quad\Longrightarrow\quad S\vdash BA,\qquad\text{an external rule;}\\
& S\vdash B(A\to C)\to(BA\to BC);\\
& S\vdash BA\to B(BA).
\end{aligned}
$$
The last two conditions are internal theorems, not rules authorizing reflection from $BA$ to $A$.
Here $P(x)=\exists y\,\operatorname{Prov}(x,y)$ numerates the theorem set by the given assumption. If $S\vdash A$, its proof supplies a genuine natural-number witness, making $BA$ a true <Sigma-1 formula>. <Sigma-1 completeness> gives $S\vdash BA$, proving the first condition. The second condition is supplied explicitly. Since $BA$ is itself a <Sigma-1 formula>, the given formalized <Sigma-1 completeness> yields $S\vdash BA\to B(BA)$, the third condition. Thus \b[the specified existential proof predicate is an <arithmetical provability predicate>].
Back to article page
