1
$\begingroup$

Is there any computable function $f(n)$, which given any integer $n$ has been proven to return either $0$ or $1$ in finite time, and for which the statement "$f(1), f(2), f(3),\ldots$ contains arbitrarily large sequences of $0$'s" has been proved to be undecidable in PA or ZFC?

If not, is there any proof of the existence or non-existence of such a function?

Edit: Is there one which is also morally undecidable?

  • 2
    What is meant by "morally undecidable"?2011-10-16

2 Answers 2

4

Let $G$ be a Gödel sentence (with intuitive meaning "I cannot be proved"), and take $$f(n)=\cases{0&\text{if }G\text{ has a proof with Gödel number }

2

Let $G(n)$ be the Goodstein sequence with first element $n$, and take $$f(n)=\cases{0&\text{if }0 \ \text{is an element of} \ G(n) \\1&\text{otherwise.}}$$

EDIT: ZFC proves the statement $\unicode{8220}f(n)=0\text{ for all }n\unicode{8221}$ and also proves that that statement cannot be proved in PA. However, this alone might not imply that PA can't prove the weaker statement $\unicode{8220}f(1),f(2),f(3),\ldots$ contains arbitrarily long sequences of $0\text{s}\unicode{8221}.$ Since I don't know whether PA can in fact prove the latter (weaker) statement, I'm unsure whether my above answer is correct after all.

  • 0
    Do you mean: undefined otherwise, and we know that doesn't happen, and we were not asked that that prove is in PA? - I don't see how it could work otherwise.2016-06-21
  • 0
    @ChristianSievers - I think you've noticed a flaw in my answer, and I don't see how making $f$ "undefined otherwise" will fix it (as the "otherwise" case seems irrelevant). Although PA can't prove "$f(n)=0$ for all $n$" (as ZFC can), that fact alone does not, of course, imply that PA can't prove the weaker statement "$f(1),f(2),f(3),\ldots$ contains arbitrarily long sequences of $0$s". (I don't know whether PA can prove the latter statement, so I'm not sure what I was thinking when I posted this answer.)2016-06-22
  • 0
    Without already using the proof that eventually 0 appears in the Goodstein series, I don't see how to show that your function is computable, while "undefined otherwise" is simple. I thought "arbitrarily long sequences of 0s" implied that all is zero, but that is indeed a different problem.2016-06-23