TODO (for the occasional passer-by): add a nice, descriptive intruduction.

'''intruduction''' ''... that's an interesting word; like an intrusive introduction, perhaps? :)'' [A FreudianTypo.]

----

I believe the CretanParadox is the first known historical example
of a (putative) logical antinomy.

----
''Here is the first paradox, originally posted on UnknowableNumbers:''

When you start trying to formalize notions like the one on this page so as to avoid "set of all sets" type paradoxical specifications, you'll probably consider definitions based on ideas of computability or proof. Then you can get into many fun situations. If you like to try thinking precisely about such things, here's a little poser for your amusement.

From KurtGoedel's work, it's well-known that we can formalize notions of mathematical reasoning and proof, and that proofs can be encoded by numbers and mechanically checked by a program. Further, from the idea of a universal TuringMachine, we know that programs can be encoded by numbers too, and can simulate other programs given their numbers. So let's build a machine M that does the following when given the input number m:

M begins to enumerate p = 0, 1, 2, 3, ... For each such number p, it first checks whether p encodes a valid proof. If not, it moves on to the next p. If p is a valid proof, M sees whether p proves that the machine represented by m, when given as input the number m, halts. If p is such a proof, then M goes into an infinite loop. If p does not prove that m(m) halts, then M sees whether p is a proof that m(m) does not halt. If p is such a proof, then M halts. Otherwise, p is a proof of some other theorem, and M goes on to the next p. Now since checking a candidate proof is a finite process, M will eventually consider all possible proofs of whether or not m(m) halts. Either it will find a proof, or there does not exist a proof either way, and so M will just run forever on input m.

Now M itself is encoded by a number, which for conciseness we'll also call M. In the usual manner of these things, we investigate M(M). Does M halt on input M? Well, if it does, then there is a trivial proof of this fact. Specifically, the proof could just list the finite number of steps that M makes when running on input M. So if M(M) halts, that can definitely be proved. But then, when M is running on input M, it would eventually discover this proof, and by the definition of M, it would then go into an infinite loop. So if we assume that M(M) halts, we have a contradiction.

Hence we have proved that M(M) must not halt.

But now we seem to be in some trouble. After all, we have just constructed a finite proof that M(M) does not halt. By the definition of M, it will eventually discover this proof, and then it will halt!

So mathematics is inconsistent, and all of CategoryMath vanishes in a puff of smoke.

Or does it :-)?

'''Discussion?:''' 

I think that I spotted the problem. You assume that the input to a TuringMachine is finite. I assume that by "input" you mean "the contents of the tape at the beginning of the program" (that's the only way to pass input to a TuringMachine). But the TuringMachine's tape is infinite, so the number of possibilities of contents of the tape is uncountable, therefore cannot be represented by a NaturalNumber, so your theorem collapses, and CategoryMath stays alive. -- AmirLivne

No. The input in the argument is always just an integer. You seem to have been confused by the use of M for both the TuringMachine and the integer which represents it.

I understand that any TuringMachine can be represented by a Natural number, by I the tape area should be infinite, therefore the number of possibilities of the contents of the tape is uncountable, therefore cannot be represented by a Natural number. -- AmirLivne

Eh? Is 'by I' a typo? Anyway, the TuringMachine (program) is finite, so there are only a countable infinity of them. The tape is as long as needed, but the relevant initial input on it is just M, an integer.

If there are an infinite number of ones on the tape, it is non-integral (e.g. 1010101010...).  I believe this is what Amir is talking about. But that doesn't count as a proper Turing execution, does it?

Since the input is M, an integer, it needs only a finite amount of tape. It's unlikely that Amir thought otherwise.

I think that when I wrote "by I" I meant "but", and my stubborn fingers rephrased it. The TuringMachine program is indeed finite, so there are only aleph-0 of them. The program can access only a finite part of the tape if it terminates, but this part is ''unbounded''. Therefore, we have to "initialize" an infinite number of cells on the tape, thus there is an uncountable number of possibilities, so the input cannot be presented as a NaturalNumber, and the machine presented in the paradox is incorrect. -- AmirLivne

Umm...Amir, if there are only finitely many non-zero cells than there are only countably many possible tapes, regardless of whether the tape is infinite or not.  The straightforward matching with the natural numbers does get everything, after all.

 0 <-> 000000000....
 1 <-> 100000000....
 2 <-> 010000000....
 3 <-> 110000000....

Incidentally, you can see that a diagonalization won't work unless we allow for combinations with an infinite number of ones.  The set of all possible infinite tapes is uncountable but this set is much, much smaller.

But you aren't limited to a finite number of non-zero cells. The program can only access a finite number of cells, but this can be 10 cells, 100000000 cells, or 6465748^235634! cells. In any can, you need to provide initial values for all of them, and there can be an infinite number of non-zero cells, so you can diagonalize on them. -- AmirLivne

Ok, so then you are indeed saying that the input can be non-integral.  I don't think in that case what you are doing counts as a proper execution of a Turing program.  It certainly doesn't count as one for the purposes of the discussion on UnknowableNumbers; any number can be specified by an infinite number of digits, but that isn't the issue.

For the paradox, one isn't limited to a ''specific'' finite number of pre-initialized non-zero cells for the input, but each input considered needs ''some'' finite number of non-zero cells.
----

''... it first checks whether p encodes a valid proof.''

And how do you know this needs only a finite amount of time?

''... because p encodes something finite (if it encodes anything), the number of methods of proof is finite, etc.''

What do you exactly mean by "p encodes something finite"? Do you mean that a decoded "proof", even if invalid, always produces a finite sequence of inference steps? Can you show then that such a code can be used to encode all the valid proofs?

''Yes. A valid proof has to be finite, and the coding (see Goedel's paper for full details) encodes any finite purported proof. Such "proofs" are countable, so this is not hard to accept.''

Well, could you just provide an algorithm that can recognize invalid "proofs" in a formal logic powerful enough to express the "proofs" of the paradox itself?

''That's exactly what Goedel's theorem is about: representing proofs in the integers system, and saying various things about proofs. Goedels methods are strong enough to check if some proof is valid, and if it says something that interests you. Goedel's proof also talks about a general way to build algorithms that check the validness of proofs. The problem is that they turn out very long and complex.''

Goedel's theorems that I know of neither say anything about "invalid proofs", nor need their own proofs to say anything about "invalid proofs". What is the theorem you are speaking about?

''The point is that Goedel converts relatively arbitrary formal mathematics into elementary arithmetic. There are various implications regardless of whether the particular phrase "invalid proof" is used.''
----

You say ''By the definition of M, it will eventually discover this proof, and then it will halt!''

But will it? What guarantee is there that M will be able to recognize this particular proof when it comes across it? To put this another way, you have proved that the statement "M(M) does not halt" is true, but you have not proved that it is provable in a formal system that M understands. In fact, it isn't, and this is what GoedelsIncompletenessTheorem is about.

''I wonder if the originator of the poser would care to comment on that.''

I am not the originator, but you '''can''' algorithmically check the validness of a proof, because of how the formal logic system is built. You can also check for patterns in the "result" of the proof, to see if it says something about whether some TuringMachine halts or doesn't halt, because you don't need to check any proof that proves that, only proofs that are of a pattern that you can recognize. The standard arithmetic system suffices for this, as much as it suffices for handling formal logic (in GoedelsIncompletenessTheorem), because all you need to do is to spot patterns in numbers. And a TuringMachine can abstract and reason about arithmetics (antromorphically). Even your hand calculator can. So I think that this is not a problem in the poser. -- AmirLivne

{''Fine, but nobody said it was. You're misunderstanding the preceding point.''}
----

To restate my point above "But will it? ..." in a different way.

GoedelsTheorem implies that in any formal system of sufficient complexity, it is possible to write true statements that are not provable within the system. M is a formal system, and the argument at the top of this page demonstrates an example of a true statement in M that is not provable in M.

The ShadowsOfTheMind book examines this question in great detail, and goes on to argue that human mathematicians are not formal systems, and that the mathematical potential of Turing Machines is limited. (I.e. it is scepitical of strong AI). A fascinating read.

JoeOtten

----

I am the originator.  The point about whether M will recognize the proof is essentially right, though the phrasing above obscures the question about where the flaw is in the initial argument more than needed.  If you want to keep thinking about it, don't read the next paragraph.

SPOILER AHEAD: ''Well, if it does, then there is a trivial proof of this fact. Specifically, the proof could just list the finite number of steps that M makes when running on input M. So if M(M) halts, that can definitely be proved. But then, when M is running on input M, it would eventually discover this proof, and by the definition of M, it would then go into an infinite loop.''  Actually M cannot discover such a trivial proof that it runs in a finite number of steps.  Why?  Because the number of steps it would use in checking the proof is bigger than the proof itself, which purports to be a listing of the steps M makes on input M.  This (deliberately hidden) self-reference invalidates the original argument.

Moving beyond this flaw, the idea is still paradoxical.  After all, the machine is sitting there grinding out all possible proofs, and if it ever halts (by finding some other sort of proof that it doesn't), we'd be in obvious trouble.  So it must not halt.  But then, haven't we ''again'' just proved that it doesn't halt, and if so, why doesn't the machine discover this proof and halt?  Or to put it another way, where's the flaw in this paragraph?  Now you'll have to excuse me, since I've just developed a brain cramp :-).
----
You've developed a brain cramp because Godel was wrong. I am sitting on a proof for this theorem: "There exists a set of laws of physics that permit the construction of a supercomputer that can solve the halting problem for both the Turing machine and itself."
----
CategoryMath