= Solution
A <logical formula> $D(\vec x,y)$ weakly defines a total numerical <function> $f$ in $S$ if, for every standard input <tuple> $\vec n$ and $m=f(\vec n)$,
$$
S\vdash D(\bar{\vec n},\bar m),\qquad
S\vdash\neg D(\bar{\vec n},\bar r)\quad(r\ne m).
$$
<Strong definability of a numerical function> additionally requires the internal uniqueness statement
$$
S\vdash\forall y\,(D(\bar{\vec n},y)\to y=\bar m).
$$
Together with the positive instance, this is equivalent to proving $\forall y(D(\bar{\vec n},y)\leftrightarrow y=\bar m)$ for each standard input. The <universal quantifier> is the extra strength: it covers nonstandard potential outputs in <first-order models> of $S$. These are the weak and strong <function> conventions used here. https://www.brucewatkins.org/math/docs/Smullyan.pdf[Gödel's Incompleteness Theorems, printed page99, definition of weak and <strong definability of a numerical function> of <functions>]{ref}
Suppose the graph of the total <function> is Sigma-1. Its complement is also Sigma-1, since
$$
f(\vec x)\ne y\quad\Longleftrightarrow\quad
\exists z\,(f(\vec x)=z\wedge z\ne y).
$$
Replace the graph assertion on the right by its Sigma-1 definition; <existential quantifiers> can be collected into one block. <Bounded completeness of an arithmetic theory> supplies numeralwise stage enumerators for each of these two disjoint complementary <sets>. Apply (b) to them. Its separating <logical formula> is provable exactly at the required graph <tuples> in the positive direction and refutable at all the other standard <tuples>, proving <weak definability of a numerical function>.
Using the graph <logical formula> alone would only supply positive instances from true existential witnesses; the separation construction is what supplies the negative-instance <formal proofs> without assuming <Sigma-1 soundness> or completeness for false Sigma-1 statements.
Back to article page
