Function which is weakly provably definable, but not provably definable

Question

All of the following is in the standard language of $\mathsf{PA}$ (or whichever you think this is -- I doubt it makes a difference); $\overline{n}$ indicates the numeral term of an $n \in \mathbb{N}$.

Call a function $g \colon \mathbb{N}^k \to \mathbb{N}$ weakly provably definable from assumptions $S$ if and only if there is a formula $\varphi(v_0, \ldots, v_k)$ such that

1. if $(n_0, \ldots, n_k) \in \mathcal{G}_g = \{ (n_0, \ldots, n_{k-1}, g(n_0, \ldots, n_{k-1}) \mid n_i \in \mathbb{N}\}$, then $S \vdash \varphi(\overline{n_0}, \ldots, \overline{n_k})$;
2. if $(n_0, \ldots, n_k) \notin \mathcal{G}_g$, then $S \vdash \neg \varphi(\overline{n_0}, \ldots, \overline{n_k})$.

Further, call $g$ provably definable from assumptions $S$ if and only if there is a $\varphi$ such that for any $n_i \in \mathbb{N}$ $$S \vdash \forall v_k \left(\varphi(\overline{n_0}, \ldots, \overline{n_{k-1}}, v_k) \leftrightarrow v_k = \overline{g(n_0, \ldots, n_{k-1})}\right).$$

It's quite quick to see that if $g$ is provable definable from $S$ then it is weakly provably definable from $S$ (simply take the same $\varphi$).

It seems fairly natural though that the latter should not follow from the former, the point being that when $g$ is provably definable, we can see 'all' of its values, whereas when it is just weakly provably definable, we may only check particular instances. Is there an obvious example to show this?

---

NB: I previously had a silly definition for weak provably definability which entailed -- by an answer below -- that all functions were wpd. For completeness (and so the below makes sense) the incorrect definition was that $g$ was wpd from $S$ iff there was a $\varphi$ such that

1. if $S \vdash \varphi(\overline{n_0}, \ldots, \overline{n_k})$, then $(n_0, \ldots, n_k) \in \mathcal{G}_g = \{ (n_0, \ldots, n_{k-1}, g(n_0, \ldots, n_{k-1}) \mid n_i \in \mathbb{N}\}$;
2. if $S \vdash \neg \varphi(\overline{n_0}, \ldots, \overline{n_k})$, then $(n_0, \ldots, n_k) \notin \mathcal{G}_g$.

Answer 1

The main point here is to notice that wpd proves that the theory decided all standard instances, so of course, to find wpd that is not pd one need to find a theory that fails at some nonstandard level, but not at any standard level. To do this we can "artificially" make any function wpd:

Let $g$ be any non-provably definable function in PA. If it is weakly provably definable in PA, we are done, if not:

Let be $L=L_{PA}∪\{P\}$ where $P$ is $n+1$-ary relational symbol.

Let $S$ be $PA$ together with an axiom for each term (i.e. standard natural) that states that $P$ calculate $g$ correctly.

Now $g$ is trivially wpd from $S$.

We need to show that $g$ is not pd from $S$: For each $φ∈L_{PA}$ let $M_φ$ be a nonstandard model of PA that witness the fact that $g$ is not pd by $φ$, add the symbol $P$ (with the correct interpretation on the standards), we will interpret $P(\ldots, x,\ldots)$ to be true for every nonstandard $x$ (that is, $P$ is true if there is any non-standard value that appears in it), call this new model $M_φ'$.

Let $w_{φ}$ be a witness to the failure of $g$ being pd from $φ$ in $M_φ$ (that is, $w_{φ}$ is nonstandard and $M_φ⊨φ(n_0,\ldots n_{k-1}, w_φ)$ for some standard $n_i$).

Given $ψ∈L$, Transform any appearance of $P$ in $ψ$ as follows (whenever I say "True", I mean "0=0", and for "False" I mean "0=1"):

• If $P(n_0,\ldots,n_k)$ appears for terms $n_i$, replace it with the truth value of the statement (It is well defiend as the theory decides it)
• If $∃z∀x∃w(... ¬P(\ldots, x',\ldots) ...)$ appears, replace $¬P(\ldots, x',\ldots)$ with False
• If $∀z∃x∀w(... P(\ldots, x',\ldots) ...)$ appears, replace $P(\ldots, x',\ldots)$ with True
• If $∀x(... P(\ldots, x',\ldots) ...)$ appears, and it is not of the forms previously defined, replace $P(\ldots, x',\ldots)$ with the truth value of this statement in the standard model
• If $∃x(... ¬P(\ldots, x',\ldots) ...)$ appears, and it is not of the forms previously defined, replace $¬P(\ldots, x',\ldots)$ with the truth value of this statement in the standard model

In here, $z,x,w$ can be tuples (maybe empty), and $x'$ is just a subset of $x$ (not empty).

Call this transformed formula $ψ'$. Notice that $ψ'$ is in the language of $L_{PA}$, furthermore, notice that $M_{ψ'}'$ thinks that both $ψ'$ and $ψ$ always agree with one another.

So, if $g$ was pd from $S$, it would have been witnessed by a formula $ψ$, such that:

\begin{align*} M_{ψ'}'&⊨∀x \left(ψ(\overline{n_0}, \ldots, \overline{n_{k-1}}, x) \leftrightarrow x = \overline{g(n_0, \ldots, n_{k-1})}\right) \\ M_{ψ'}'&⊨∃x \left(ψ'(\overline{n_0}, \ldots, \overline{n_{k-1}}, x) \land x ≠ \overline{g(n_0, \ldots, n_{k-1})}\right) \\ M_{ψ'}'&⊨∀x \left(ψ(\overline{n_0}, \ldots, \overline{n_{k-1}}, x) \leftrightarrow ψ'(\overline{n_0}, \ldots, \overline{n_{k-1}}, x)\right) \end{align*}

Contradiction.

---

Answer for before the editted question

There is obvious example, but it has a very boring reasoning:

Every function is weakly definable from $PA$.

To see this, let $ψ$ be any independent statement in $PA$, and let $φ(a_0,...,a_k)=ψ$: $S \nvdash \varphi(\overline{n_0}, \ldots, \overline{n_k})$ and $S \nvdash \lnot\varphi(\overline{n_0}, \ldots, \overline{n_k})$, so $g$ is vacuously weakly provably from $PA$.

---

The actual difference between your 2 definition is not about "how many elements it checks", but the fact that in the weakly definition we only care about $\rightarrow$ and in the other definition we also care about $\leftarrow$