Does there exist a valid first-order formula whose Skolemization is satisfiable only with uncomputable functions?

Question

Let $F$ be a valid first-order formula. Then the Skolemization of $F$, let's denote it by $F_S$, is at least satisfiable. Let's say $F_S$ contains function symbols $f_i$ for $1 \leq i \leq n$, for some $n\in\omega$. Does there exist a formula $F$ such that $F_S$ is true only when each of $f_i$ is interpreted by some uncomputable function $\mathcal{M}^{f_i}$?

Answer 1

Not quite/not yet an answer to your question about valid formulas, but:

This is true anyway for satisfiable formulas, in models of a theory $\mathscr{T}$ such as PA with "enough arithmetic" to talk about syntax, or equivalently, Turing machines. Start with the Kleene T-predicate:

$T(e,x,y) \iff$ $e$ encodes a Turing machine $M$, $y$ is a terminating computation of $M$ on input $x$.

T is arithmetical (even primitive recursive). A formula representing the Halting Problem, a complete semi-computable (r.e.) set, is: $$ K(e) \iff \exists y \, T(e,0,y) \text{.} $$

The following is a theorem: $$ \vdash \forall e \exists z\,((z = 1 \wedge K(e)) \vee (z = 0 \wedge \neg K(e)) \tag{$S_1$} $$

In any model of $\mathscr{T}$, any Skolem function $f(e)$ for $z$ will "solve" the Halting Problem and is not computable. It's Turing degree is $\mathbf{0'}$. Similarly, by using $K_n(e)$ instead of $K(e)$ where $K_n(e)$ is a formula representing a $\Sigma^0_n$-complete set, a Skolem function for the analogous sentence will have degree $\mathbf{0^n}$.

The definition of $T$, and thus of $K$, uses only finitely many axioms $\mathscr{T_0}$ of $\mathscr{T}$, so one could form the sentence $\vdash \bigwedge \mathscr{T_0} \to S_1$. Among the models will be nonstandard models of $\mathscr{T}$ — say, nonstandard models of PA; by a result of Tennenbaum, in such models even $+$ and $\times$ are non-computable. However, this sentence will also have models that aren't models of $\mathscr{T}$, because not every instance of the induction schema is in $\mathscr{T_0}$. In those models, it might not even be clear what "computable" means.

Answer 2

I believe the answer to my question is no, there are no such formulas. The reason is somewhat trivial.

If $F$ is a valid formula, then it's also satisfied on a model $\mathcal{M} = (D, I)$ where $|D| = 1$. There is just one possible variable assignment $v$ on such model: $v(x_i) = d$, where $d$ is the only $d \in D$. Because of this, both $\forall x \phi(x)$ and $\exists x \phi(x)$ have the same truth value (according to $\mathcal{M}$) as just $\phi(x)$. If we assume w.l.o.g. that $F$ was in prefix normal form, then $F$ with no quantifiers is the same as $F_S$ with no quantifiers, with the exception of $F_S$ having certain Skolem function (sub)terms instead of variables. However, every term regardless of content is interpreted as $d$, and so this syntactic difference makes no difference for evaluation. Since $\mathcal{M}\vDash F$, it follows that $\mathcal{M}\vDash F_S$. All the functions are projection functions, which are computable.