Is Fkk Actually True

After reading GoedelsIncompletenessTheorem, you may wonder whether this magical proposition Fk(k) is actually true or not. At least on Wiki, there is no agreement over this important issue.

No, we don't "know" that Fk(k) is true at all. In fact, we have a choice here: we can add the proposition Fk(k) as a new axiom to our system, but we can also add ~Fk(k) as a new axiom! In that case, the new axiom tells us that there actually *is* a number x so that Px proves Fk(k). This seems worrying, but it isn't. It would be worrying if we could prove that Ex[Px proves Q] => Q. But we cannot; the best we can do is construct an infinite number of proofs of the form [P0 proves Q] => Q, [P1 proves Q] => Q, etc.. One way to think of it is to say that the new number x is infinite, and we actually only have proven that Ex[Px proves Q AND x is finite] => Q. In other words, we have an infinite "proof" for Fk(k), but only finite proofs really count.

No, we don't "know" that Fk(k) is true at all.

Yes, we do. Fk(k) says in effect "I can't be proven by the system". If it turns out the system can in fact prove this statement, then it is inconsistent, because it has "proven" something which isn't true. Some systems (in fact infinitely many) have this undesirable property. If on the other hand it turns out the system cannot prove the statement, then by definition it is true, so the system is incomplete. It would be nice if we could have systems that were both consistent and complete, but Goedel's theorem proves that is impossible, at least for sufficiently interesting systems.

In fact, we have a choice here: we can add the proposition Fk(k) as a new axiom to our system, but we can also add ~Fk(k) as a new axiom! In that case, the new axiom tells us that there actually *is* a number x so that Px proves Fk(k).

This can be true, depending on the system, but this has no bearing on the truth or otherwise of Fk(k). The system cannot decide whether Fk(k) or ~Fk(k) is true. Either hypothesis is consistent with the system. Only Fk(k) is true however.

-- MartijnMeijering

If it turns out the system can in fact prove this statement, then it is inconsistent, because it has "proven" something which isn't true.

This is not the definition of inconsistent. A system is inconsistent when both P and ~P are valid propositions in the system (for some proposition P). "Mathematical truth" doesn't enter the definition. Indeed, the whole concept of "inconsistent" would be worthless if it did.

You're right, this didn't feel right when I typed it in. I remember there was a difference between consistent and omega-consistent. I'll look it up tonight. -- MartijnMeijering

Only Fk(k) is true however.

Apparently you have some definition of true other than provable in some agreed-upon consistent formal system.

Certainly, that's the whole point of the theorem, every consistent system has undecidable sentences. We're comparing derivable by the system to true according to some external definition. If I remember correctly there are more subtleties here.

However, I'm not aware that the truth of Fk(k) is proclaimed somewhere in the Bible, and the only other way I know to assert truth of a statement, namely by mathematical proof, can be shown to be inapplicable in this case. Fk(k) says that much.

-- StephanHouben

That's not what Fk(k) says. It says it is undecidable for the given system, not mathematics in general. I don't understand why you question the truth of Fk(k). Are you suggesting that the system can in fact prove Fk(k)?

I'll try to restate my point again, and to explain exactly where it differs with the point of view of a Platonist.

I hope we all agree about the following:

So we cannot prove Fk(k) within the formal system, but perhaps we can prove it outside it, as MartijnMeijering suggested. Such a proof would go as follows:

Suppose that Fk(k) weren't true. Then we have ~Fk(k), which says that there is a proof P for Fk(k). So we have a proof P for Fk(k), so we find that Fk(k) is true. But that is in contradiction with our assumption that Fk(k) is not true. So our original assumption leads to a contradiction, and is therefore untrue. Thus Fk(k) is true.

Note that this is a proof from the absurd. It uses the principle of "Tertium Non Datur", i.e. "There is no third", a statement is true or false, no third possibility exists. Perhaps this comes as a surprise to some of you, but this principle is not accepted by all mathematicians. Typically, people who call themselves Platonists consider it to be true. But people like Brouwer reject this principle, and would therefore not accept the truth of Fk(k).

Note that - to a non-Platonist - acceptance of ~Fk(k) doesn't lead to a paradox at all. After all, ~Fk(k) says there is a proof P for Fk(k), but as long as you cannot actually show me this proof P, I will not accept Fk(k).

-- StephanHouben

No, that's what it doesn't. Fk(k) implies that no natural number is the proof number of Fk(k). It could be true and have an... uh... supernatural proof number. Nothing in the axiomatic system rules out supernatural numbers. They don't exist in the standard model, but there are other models. Fk(k) is not true in every model, so in short it is not true.

Above I wrote You're right, this didn't feel right when I typed it in. I remember there was a difference between consistent and omega-consistent. I'll look it up tonight.

I haven't fully digested all the material yet, but I've been rereading Raymond Smullyan's excellent discussion of Goedel's theorems in http://www.amazon.com/exec/obidos/ASIN/0195046722.

Smullyan presents three different proofs. The first is based on the correctness of Peano arithmetic. The second (Goedel's original proof) is based on a weaker assumption, the omega-consistency of Peano arithmetic. A third proof requires only the consistency of Peano arithmetic.

Smullyan gives the explicit construction of the Goedel sentence Penrose considers too hard for the average reader to understand. Fortunately it's really rather straightforward for a programmer. It's like programming, only in a programming language that's more powerful than a Turing machine. I've been thinking about turning this into some kind of a programming assignment, but I'm not sure it can be done. I'll let you all know when I know more.

StephanHouben writes:

But people like Brouwer reject this principle, and would therefore not accept the truth of Fk(k).

Actually, I think this argument would be acceptable to intuitionists. Fk(k) is really a statement about numbers. By construction it turns out to be equivalent to the assertion that it cannot be proved within the system, but it can be considered separately. If I'm not mistaken, intuitionists object to existence proofs by contradiction, not proof by contradiction in general. But perhaps I am mistaken. At any rate, I remember reading somewhere that Goedel deliberately constructed his proof in such a way that it was acceptable to intuitionists.

-- MartijnMeijering

Note that - to a non-Platonist - acceptance of ~Fk(k) doesn't lead to a paradox at all. After all, ~Fk(k) says there is a proof P for Fk(k), but as long as you cannot actually show me this proof P, I will not accept Fk(k) (and thus get a contradiction).

I've been thinking about this some more. The self-referential aspect of Fk(k) keeps confusing me. At first I wanted to say this:

You say you will not accept Fk(k) until you have seen P. Shouldn't that be ~Fk(k)? You seemed to be saying "I'll only believe Fk(k) can't be proved if you showed me a proof". That doesn't make sense to me.

However, by construction, Fk(k) doesn't only say "Fk(k) can't be proved" , it also says "Fk(k) is true". If we substitute that in the above we get:

You seemed to be saying "I'll only believe Fk(k) is true if you showed me a proof".

That makes more sense to me.

I'll have to think about this some more...

One of the issues is whether a proposition of the form "there is a proof P for proposition Q" allows you to accept Q. According to the rules of our formal system, the answer is no. After all, if this were the case, we could derive a contradiction (i.e. we could prove Fk(k), as sketched above, which says there is no proof. Contradiction!) So such a rule would make the system inconsistent.

By the way, there is some relation with the HaltingProblem here. We can create a Turing machine which enumerates all valid propositions in a formal system. We can then, of course, also construct a Turing machine which enumerates all propositions which can be proven to be invalid (i.e. those P's for which we can prove ~P). If a formal system was both consistent and complete, then both Turing machines could be used together to determine for a given P whether it is true or not. Since we can write the HaltingProblem for a given Turing machine T as a problem in Peano number theory (imagine long technical proof here), we would effectively have solved the HaltingProblem. Which is a no-no.

We have to be very careful to distinguish between truth and derivability in some particular system. The whole point of Goedel's theorem is that these notions are different. Every useful system (in a sense that can be made precise) has sentences that are fundamentally undecidable. It would be consistent to assume ~Fk(k). I believe that even though it would not contradict any of the sentences of our system, it would nevertheless not be correct. You seem to be challenging the validity (or acceptability to intuitionists) of the proof given on GoedelsIncompletenessTheorem. [No, GoedelsIncompletenessTheorem is a completely constructive proof. However, GoedelsIncompletenessTheorem itself doesn't say anything about the truth of Fk(k).]

To come back to your question One of the issues is whether a proposition of the form "there is a proof P for proposition Q" allows you to accept Q.. Perhaps not within the system itself, but if the derivation system is sound you and I would obviously have to accept it. If I'm not mistaken, Goedel's construction allows you to encode the notion of provability in (intuitionistic?) first order logic combined with the axioms of Peano arithmetic within that system itself.

Historically, Goedel's theorem was an answer to one part of the Hilbert program. Hilbert's idea was to unify the viewpoints of platonists and intuitionists by proving (in a constructive way) that mathematics was both consistent and complete. If we had a constructive proof of that, then intuitionists would effectively have a constructive proof of the "tertium non datur" principle! After all, in a consistent and complete formal system, for every P either P or ~P is true. So what Goedel showed was that this idea of Hilbert was impossible to carry out.

You seem to be challenging the validity (or acceptability to intuitionists) of the proof given on GoedelsIncompletenessTheorem. [No, GoedelsIncompletenessTheorem is a completely constructive proof. However, GoedelsIncompletenessTheorem itself doesn't say anything about the truth of Fk(k).]

Stephan, at first I thought you were confusing Fk(k), which in a sense is a theorem of number theory, with the meta-statement "Fk(k) cannot be proved by the system", which, miraculously, is logically equivalent. To clear up the presumed confusion, I tried to explain how Fk(k) is constructed. Someone kindly pointed out a rather serious mistake I had made in the explanation. Were you that person? If so, you probably know more about the subject than I do.

So, I'll try barking up a new tree now. You say that GoedelsIncompletenessTheorem doesn't say anything about the truth of Fk(k). Raymond Smullyan gives a number of proofs of Goedel's theorem. He starts with a proof that is based on the correctness of Peano arithmetic, then a proof which only requires it to be omega-consistent and finally a proof which only requires it to be consistent. I've only studied the first proof in detail. Are you saying that only the second and third proof are acceptable to intuitionists and that they do not (intuitionistically) prove the truth of Fk(k)? -- MartijnMeijering

I think that Fk(k), interpreted as a theorem in Peano arithmetic, can be proven to be true under the assumption that Peano arithmetic is omega-consistent. (Since the addition of ~Fk(k) to the formal system makes it omega-inconsistent, however still consistent.) Frankly, I probably need to read up on this subject. -- StephanHouben

There's a fundamental misunderstanding in the "meaning" of Fk(k) at work here. In essence, it says "There is no natural number that denotes a proof for this sentence." Goedel showed, that there is neither proof nor disproof for this proposition within the system. The question, whether Fk(k) is true, is something separate.

It is possible to construct a model for number theory, where Fk(k) is true. This is the standard model, where there are only natural numbers and there are no proofs that have no proof number. A model where Fk(k) is false is also possible. It would have to include "SurrealNumbers", which are best imagined as being "greater than infinity". These would denote more proofs, again best imagined as consisting of infinitely many steps. So after all Fk(k) is not true or false in every model, and "going outside the system" or "applying insight" or even "CONSCIENCE" or something won't change that fact.

Such a model might be considered inelegant or counterintuitive, but nothing in number theory rules out non-standard models. To do so, one would have to express the absence of unnatural numbers somehow. I don't think this is possible in first order logic, and I believe increasing the power of the logic only moves the problem up one order, thus creating a new Fk(k). -- AnonymousDonor

Here's one approach that seems to do well when introducing Goedel and associated material.

Now we map red to non-syntactic, white to syntactically valid propositions, red dots to "false", blue dots to "true", and talk about Fk(k). Introducing any concept of "truth" as late as possible avoids so much baggage.

So... the interesting question: Does GoedelsIncompletenessTheorem mean that there will be (for a sufficiently complex system--you left out that qualifier) white strings to which we cannot assign dots? Or does Goedel mean that there are white strings which "obviously" have blue dots, but which we cannot prove that they are blue? This gets back to the question of IsFkkActuallyTrue: Can we assume either Fkk or !Fkk, add that as an axiom to the system, and still get a consistent system? Can we show that one of Fkk or !Fkk leads to an inconsistent system (which, if we allow the excluded middle, would prove the opposite proposition?) Or does assuming either Fkk or its inverse lead to inconsistency? Might it be the case that Fkk is a RED string and not a white one?

There are two cases (inconsistent and/or incomplete).

The incomplete case is thus:

If the strings are already "out there" with the dots sticked on it, that means we are talking about a model. Now because the model will be an infinite set, this breaks the appeal to intuition. Intuitively you may imagine that you'll see a string with a blue dot on it (or red , it doesn't matter) and you'll stare at it long enough and tell to yourself: "I cannot know if the color of this dot is the right one". You want to verify that the dot on it is the correct one according to the given rules, but you simply cannot. So you won't know if that set of strings is really a model or not.

If you twist the setting on its head you can say like this: you're given all the white strings, you're given a few with dots on them (the axioms) and a set of rules that you can follow to put dots on more strings. So there's this odd string of a finite length, but :

a) if you follow the rules from the initial set and assign more and more dots , you'll never reach that string. You may circle around it, jump up and down, but you'll never get to it. Contrast this with a rule for coloring the prime versus non-prime natural numbers according to Erathostenes. If you start from 2, no matter how long is a particular string, you'll always be able to determine what you should stick on it. But the Game of Erathostenes is easy. The Game of first order logic is damn hard. About the Fkk string the important thing is that you know (because it is constructed on purpose) that your game will never get to it. The fun part is that if somebody hands you a string at random, you may end up not knowing if you'll color it (regardless of the color) or if you should just give up. You can run lots of robots to stick dots on white strings according to the rules, and an hour passes and that string hasn't received a dot yet, and a week passes and no luck yet, and one year passes and you decide to give up. But maybe if you waited just one more second one those pesky robots would have sticked a dot on it.

b) if you stare at the string and try to figure out the path in reverse (what rules can I apply that would take me to this string? You suspect that the algorithm in the case a) may take you down an infinite loop branch that you cannot get out of, but you could be more successful if you try to find the path in reverse. And then again you won't be able to find a way out of the maze. If you run any kind of theorem prover to help, you [?] that prover will spin and spin and spin and it may not even look like an infinite loop, but it will never halt.

For the inconsistent case, the intuition is simpler. It means that you can start working on it and you'll eventually get to stick a dot on the stupid string, but if you keep working some more, you'll apply the other color as well. For some people, a white string with dots of different color is a sign of trouble.

Put it a different way, if you have an automatic theorem prover algorithm, whatever that may be, providing you know it is correct, the process will run forever, and that's the connection with the HaltingProblem.

See ItDepends

EditText of this page (last edited April 20, 2008) or FindPage with title or text search