<p>Let <span class="math-container">$T$</span> be a reasonble theory of arithmetic, say <span class="math-container">$\mathrm{PA}$</span>. Consider the sequence
<span class="math-container">$$f(m) =
\begin{cases}
1 &amp; \text{if $m$ encodes a proof of $\vdash_T 0 = 1$} \\
0 &amp; \text{otherwise}
\end{cases}
$$</span>
The sequence is clearly computable, even primitive recursive and therefore representable in <span class="math-container">$T$</span>.</p>
<p>If there is <span class="math-container">$m$</span> such that <span class="math-container">$f(m) = 1$</span> then <span class="math-container">$T$</span> is inconsistent, which is not known to be the case.</p>
<p>If <span class="math-container">$T$</span> proves <span class="math-container">$\forall m . f(m) = 0$</span> then <span class="math-container">$T$</span> proves <span class="math-container">$\neg \mathrm{Bew}(\ulcorner 0 = 1\urcorner)$</span>, i.e., its own consistency, which is not possible if <span class="math-container">$T$</span> is consistent.</p>

CC BY-SA 4.0
2021-08-23T19:32:50.110Z
2021-08-23T19:38:06.837Z
2021-08-23T19:38:06.837Z
Andrej Bauer
<p>My question concerns the property of being constant for computable functions <span class="math-container">${\mathbb N}\to \{0,1\}$</span>, within any common framework <span class="math-container">$T$</span> strong enough to include Heyting arithmetic (and of course not known to be inconsistent.)</p>
<p>Is there some particular, i.e. known, computable function <span class="math-container">$f:{\mathbb N}\to \{0,1\}$</span> such that</p>
<ul>
<li><span class="math-container">$T$</span> proves <span class="math-container">$f$</span> to be total,</li>
<li>no number <span class="math-container">$m$</span> with <span class="math-container">$f(m)=1$</span> is known (i.e. it's not actually ruled out that the function is constant)</li>
<li>but for which the statement <span class="math-container">$\ \forall n. f(n) = 0\ $</span> is actually known to
be unprovable in <span class="math-container">$T$</span> (it's known that there's no proof in <span class="math-container">$T$</span>)?</li>
</ul>
<p>Notes, thoughts, re-emphasis:</p>
<ul>
<li>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 <span class="math-container">$T$</span>. It could thus be that the <span class="math-container">$T$</span> might necessarily not have non-constructive tools in its proof repertoire. Maybe there's classical statements about <span class="math-container">$\Pi$</span> statements where const-ness is then always implied - if so we need to go weaker.</li>
<li>If the function returns <span class="math-container">$0$</span> in case some effective property <span class="math-container">$P(n)$</span> is being evaluated - e.g. some arithmetic relation between each input <span class="math-container">$n$</span> and the finite number of primes below <span class="math-container">$n$</span>, alla Goldbach - then we might quickly have a total function at hand, and there are some open questions of the <span class="math-container">$\forall n$</span> form. However, from looking around it seems in practice such problems are usually conjectured to be provable but just hard.</li>
<li>The function property of taking the value <span class="math-container">$0$</span> 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.</li>
<li>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 <span class="math-container">$T$</span> that captures the computable function, proves it total but can't prove or disprove const-ness.</li>
</ul>

<computability><nt.number-theory><proof-theory><constructive-mathematics><function>
What is a known sequence for which being constant is not provable?
Nikolaj-K
# What is a known sequence for which being constant is not provable?

(Asked by: username_0 on 2021-08-23)

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.

**Tags:** computability, nt.number-theory, proof-theory, constructive-mathematics, function


---

## 1 answers

### Answer by username_1 on 2021-08-23. Score: 6 | Accepted answer

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.


---

