My question concerns the property of being constant for computable functions ${\mathbb N}\to \{0,1\}$, within any common framework $T$ strong enough to include Heyting arithmetic (and of course not known to be inconsistent.)

Is there some particular, i.e. known, computable function $f:{\mathbb N}\to \{0,1\}$ such that

  • $T$ proves $f$ to be total,
  • no number $m$ with $f(m)=1$ is known (i.e. it's not actually ruled out that the function is constant)
  • but for which the statement $\ \forall n. f(n) = 0\ $ is actually known to be unprovable in $T$ (it's known that there's no proof in $T$)?

Notes, thoughts, re-emphasis:

  • The motivation here is to see some hard motivating cases for a conservative framework not to adopt omniscience principles. Hard in the sense that being zero is not just an open question but it's provably not provable by $T$. It could thus be that the $T$ might necessarily not have non-constructive tools in its proof repertoire. Maybe there's classical statements about $\Pi$ statements where const-ness is then always implied - if so we need to go weaker.
  • If the function returns $0$ in case some effective property $P(n)$ is being evaluated - e.g. some arithmetic relation between each input $n$ and the finite number of primes below $n$, alla Goldbach - then we might quickly have a total function at hand, and there are some open questions of the $\forall n$ form. However, from looking around it seems in practice such problems are usually conjectured to be provable but just hard.
  • The function property of taking the value $0$ everywhere can be undecidable for some class of partial computable functions, but I'm looking for a particular total function - in fact I'd hope for a short explicit algorithm that corresponds to it.
  • There's some total computable functions with unprovable properties in PA. E.g. some function constructed from the Goldstein situation is total but PA doesn't prove that. Just to avoid the this-system-knows-that-system-does-not-know situations I'm explicitly asking for a situation for just a single (possibly quite weak but standard math compatible) framework $T$ that captures the computable function, proves it total but can't prove or disprove const-ness.

Let $T$ be a reasonble theory of arithmetic, say $\mathrm{PA}$. Consider the sequence $$f(m) = \begin{cases} 1 & \text{if $m$ encodes a proof of $\vdash_T 0 = 1$} \\ 0 & \text{otherwise} \end{cases} $$ The sequence is clearly computable, even primitive recursive and therefore representable in $T$.

If there is $m$ such that $f(m) = 1$ then $T$ is inconsistent, which is not known to be the case.

If $T$ proves $\forall m . f(m) = 0$ then $T$ proves $\neg \mathrm{Bew}(\ulcorner 0 = 1\urcorner)$, i.e., its own consistency, which is not possible if $T$ is consistent.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.