We know that we cannot find an algorithm that would prove that a computable function "f" is total if it IS total. How come?

When a function is total, it must have a proof (derived from soundness and correctness of logic). And proof is a finite sequence of symbols, so why does simple enumeration through all the sequences (which ends in finite time) not provide us with a proof?

  • $\begingroup$ Do you know Rice's theorem? $\endgroup$
    – Raphael
    Aug 14, 2016 at 22:42
  • $\begingroup$ Be careful with your language. You can compute anything for "a" function since you can hardcode the answer. We know that there is no decider for totality for all computable functions. $\endgroup$
    – Raphael
    Aug 14, 2016 at 22:45
  • 2
    $\begingroup$ What does this have to do with Rice's theorem? $\endgroup$ Aug 15, 2016 at 1:19

3 Answers 3


You misunderstand soundness and completeness of logic. You think that it says:

A statement is true if, and only if, it is provable.

But it really says:

A statement is true in every model if, and only if, it is provable.

It can happen that there is a model in which a statement is true but not provable. What if you live in such a model? Then it could happen that in the model in which you live there is a total function $f$, but there is no proof that $f$ is total.

Here is a precise mathematical reason why your thinking does not work. I am going to show that, whatever formal system you are using (so long as it is a reasonable one), there is a total function which your formal system does not prove to be total.

You do proofs in some formal system $T$ (for instance, $T$ could be first-order logic and Zermelo-Fraenkel set theory) whose axioms are computably enumerable (or else you're a mystic guru). Let us also assume that $T$ contains arithmetic, and that $T$ is consistent (or else you're mad).

Define the following function f

def f(n):
    if n encodes a proof of 0 = 1 in formal system T:
        while True: pass
        return 0

Observe that f is total if, and only if, $T$ is consistent:

  • if $T$ is consistent then it does not prove $0 = 1$, hence f never enters the infinite while loop.
  • if f is total, then it never enters the infinite while loop, therefore no $n$ encodes a proof of $0 = 1$ in $T$, therefore there is no proof of $0 = 1$ in $T$, which means that $T$ is consistent.

Because $T$ is consistent, f is total.

But $T$ does not prove that f is total: if it did, then it would prove that, for every $n$, $n$ does not encode a proof of $0 = 1$, but this would imply that $T$ proves its own consistency, which it cannot by Gödel's incompleteness theorem.

Supplemental: Ideas about having multiple theories $T_0, T_1, T_2, \ldots$ are quashed by (where unpair is a bijection $\mathbb{N} \to \mathbb{N} \times \mathbb{N}$):

def g(n):
    (i, j) = unpair(n)
    if i encodes a proof of 0 = 1 in formal system T(j):
        while True: pass
        return 0

Now $g$ is total if and only if all $T_i$'s are consistent, but no $T_j$ can prove that they are all consistent (if it could, it would prove its own consistency as well).

  • $\begingroup$ can't we get around this problem by having a self trusting theory and hierarchy of theories, I mean if we have an algorithm A(x) that on input (t,n) output nth algorithm that is provable by $T_t$ theory and A((0,0))==A $\endgroup$
    – raoof
    Jan 27, 2023 at 2:09
  • $\begingroup$ Sorry, you'll have to be more precise there. What problem? And I don't understand your suggestion. $\endgroup$ Jan 27, 2023 at 10:18
  • $\begingroup$ I mean the problem that a theory $T$ can not prove it's own consistency and because of that there is always at least one computable function that can not be proven to be total, now I'm suggesting if we have for example $T_1=PA, T_2=PA+Cons(PA), ...$ and $T_0$ be an enumeration of these theories then there is an algorithm A(x) that enumerate the set of all total computable function. in other words your function f can not be proved to be total by $T=T_1$ but $T_2$ can prove it $\endgroup$
    – raoof
    Jan 27, 2023 at 11:46
  • $\begingroup$ That doesn't help, because then there will be a map f which is total if and only if all $T_1, T_2, T_3, \ldots$ are consistent, and so no $T_i$ will prove is totality. As long as you can computably enumerate whatever theory or theories you're working with, we can use the same trick to construct f. $\endgroup$ Jan 27, 2023 at 12:33
  • 1
    $\begingroup$ No problem, I updated the answer. $\endgroup$ Jan 27, 2023 at 16:06

so why does simple enumeration through all the sequences (which ends in finite time) not provide us with a proof?

That idea could maybe give you a semi-decider, but certainly not a decider -- you don't know a size bound on the proof! That is, you can never say "no, it's not total" after finite time.

Note, though, that the idea has to be fundamentally flawed; the set of total functions is not enumerable.


"It must have a proof" - no, not necessarily. For example, write a program that for each even integer n ≥ 4 finds the smallest prime p such that n-p is also a prime, and doesn't halt if such a p does not exist. This is very, very likely to be a total function. But currently there is no prove known. And it is quite possible that no prove exists.

Someone remarked that this was a weak example and not convincing. OK, the fact is that with this easy to understand problems the worlds greatest mathematicians don't agree at all that a total function would have a proof of totality. So "it must have a proof" is a claim that you are more clever than the worlds greatest mathematicians.

And someone will be able to find a total function where the existence of a proof that it is total leads to a contradiction.

  • $\begingroup$ This is a rather weak example because it relies on people not knowing the status of a certain mathematical problem. It is not going to be convincing to someone who misunderstands completeness of first-order logic. $\endgroup$ Aug 15, 2016 at 1:18
  • $\begingroup$ It's not supposed to convince - it is supposed to demonstrate that the assumption "if a function is total then there is a proof for it" isn't obvious or simple but very, very non-obvious. And it demonstrates the problem in the assumption in a very simple non-abstract way. $\endgroup$
    – gnasher729
    Aug 15, 2016 at 7:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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