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

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.