5
$\begingroup$

This question was asked and bountied at MSE without success.

For an appropriate theory $T$, say that an $n$-ary $T$-provably recursive function is a $\Sigma_1$ formula $\varphi$ with $n+1$ free variables which $T$ proves defines a total function. Terms and "near-terms" (e.g. "$\Delta_1$-piecewise combinations" of terms) are of course always $T$-provably recursive, but in general these account for only a miniscule fragment of the $T$-provably recursive functions (consider exponentiation in $\mathsf{PA}$).

I'm interested in whether $\mathsf{Q}$ has any such "surprising" provably recursive functions:

Is there any $n$-ary $\mathsf{Q}$-provably recursive function $\varphi(\overline{x},y)$ such that for every $\{+,\times\}$-term $t(\overline{x},\overline{z})$ we have $$\mathsf{Q}\vdash\forall \overline{z} \exists a\forall \overline{x}[\bigwedge_{1\le i\le n}x_i>a\implies \neg\varphi(\overline{x},t(\overline{x}, \overline{z}))]?$$

Intuitively, I'm asking whether there is a $\mathsf{Q}$-provably recursive function which is $\mathsf{Q}$-provably eventually different from every term. Note that "eventually different" here is used in the sense of "different on all inputs with each coordinate sufficiently large." In particular, a function like $$\varphi(x_1,x_2,y)\equiv (y=0\wedge x_1=x_2)\vee(y=1\wedge x_1\not=x_2)$$ is not an example; while there is no specific term to which it is eventually equal, both $0$ and $1$ are terms to which it is not eventually not equal. (I'm like $80\%$ sure I got that right.)

Improve this question
$\endgroup$
6
  • $\begingroup$ The easiest candidates for $\phi$ are formulas defining numbers near $x/2$ or $\sqrt{x}$, but then we can show that any formula like $\forall x \exists! y, \phi(x,y)$ fails in some non-standard models of $Q$. So presumably the question is how to go more generally from a purported function $\phi$ to a model where the above sentence fails. $\endgroup$
    – user44143
    Commented Sep 7, 2020 at 0:41
  • $\begingroup$ @MattF. Yes, exactly - but it's not clear to me how to do that. $\endgroup$
    – Noah Schweber
    Commented Sep 7, 2020 at 1:01
  • $\begingroup$ It might suffice to consider the model of $Q$ consisting of all elements of $\mathbb{Z}[t]$ whose non-constant coefficients are non-negative and which have at least one positive coefficient. Perhaps for any purported $\phi$ eventually always different from any term, it can be shown that $\forall x \exists! y, \phi(x,y)$ fails in this model, using $x=t$. $\endgroup$
    – user44143
    Commented Sep 7, 2020 at 1:05
  • $\begingroup$ The predecessor function is provably total in $Q$, and it is eventually different from each term in the standard model, but under its most natural definition, $Q$ does not prove the formula you want. I’m not sure if it can be reformulated so that $Q$ does prove the formula. In general, it’s extremely difficult for $Q$ to prove any two functions to be eventually different, because of black-hole models of $Q$ such as $\mathbb N\cup\{\infty\}$ here. $\endgroup$
    – Emil Jeřábek
    Commented Sep 7, 2020 at 6:19
  • 4
    $\begingroup$ Actually, the $\mathbb N\cup\{\infty\}$ model outright shows that the answer is NO, and you don’t even need $+$ and $\times$ (just constant terms): let $z$ be such that $\mathbb N\cup\{\infty\}\models\varphi(\vec\infty,z)$; then $\mathbb N\cup\{\infty\}\models\forall a\,\exists\vec x\,\bigl(\bigwedge_ix_i>a\land\varphi(\vec x,z)\bigr)$, namely $\vec x=\vec\infty$. $\endgroup$
    – Emil Jeřábek
    Commented Sep 7, 2020 at 9:40

0

Reset to default

You must log in to answer this question.