3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Do you know Rice's theorem? $\endgroup$ – Raphael Aug 14 '16 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 '16 at 22:45
  • 2
    $\begingroup$ What does this have to do with Rice's theorem? $\endgroup$ – Andrej Bauer Aug 15 '16 at 1:19
9
$\begingroup$

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
    else:
        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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

"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.

$\endgroup$
  • $\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$ – Andrej Bauer Aug 15 '16 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 '16 at 7:55

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.