What is a known sequence for which being constant is not provable?

Question

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.

Answer 1

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.