Timeline for Does $\mathsf{Q}$ have any interesting provably recursive functions?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 7, 2020 at 9:40 | comment | added | Emil Jeřábek | 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$. | |
| Sep 7, 2020 at 6:22 | comment | added | Noah Schweber | @EmilJeřábek That's a good point - it would probably be better to add monus to the language and go a bit beyond $\mathsf{Q}$. | |
| Sep 7, 2020 at 6:19 | comment | added | Emil Jeřábek | 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. | |
| Sep 7, 2020 at 1:05 | comment | added | user44143 | 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$. | |
| Sep 7, 2020 at 1:01 | comment | added | Noah Schweber | @MattF. Yes, exactly - but it's not clear to me how to do that. | |
| Sep 7, 2020 at 0:41 | comment | added | user44143 | 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. | |
| Sep 6, 2020 at 19:30 | history | asked | Noah Schweber | CC BY-SA 4.0 |