Attempt at an intuitive explanation (ELI12) for the weirdest logic theorem ever (Gödel-Carnap)
Explain me like I am 12.
When people write things like this:
The Diagonal Lemma (of Go?del and Carnap) is one of the fundamental results in Mathematical Logic. However, its proof (as presented in textbooks) is very un_intuitive, and a kind of “pulling a rabbit out of a hat”. As a matter of fact, several theorems that are proved by using this lemma now have diagonal-free proofs.
They express their (utter) dislike for this lemma.
Especially its proof is considered to be incomprehensible. That is a problem because both Gödel's first incompleteness theorem and Tarski's undefinability theorem trivially follow from this lemma. Let's attempt to come up with a more intuitive explanation anyway.
First step. We must be able to encode logic sentences as numbers.
Nowadays, doing that is actually trivial. This page is encoded in utf8. It is a perfectly suitable Gödel numbering. We do not need to use Gödel's original encoding which he designed back in the 1930ies before computers existed.
For example, %A = 65 (decimal). That means: the number for the letter A is 65.
Or %(hello) = 0x68656c6c6f (hexadecimal) = 448378203247 (decimal)
You can convert any language expression online from utf8 to hexadecimal (base=16) using this test page and then from hexadecimal to decimal (base=10) using this test page. So, whatever expression we write, in logic or in natural language, we can always represent it as a natural number.
Second step. We must be able to represent properties of logic sentences.
How do we represent the sentence, "The banana is yellow", in logic? If the predicate function yellow is computable and if it accepts a natural number as input, then this form will do the job:
banana [math]\leftrightarrow[/math] yellow(%banana)
It means that the banana has the property yellow. In general, the syntactical form, M [math]\leftrightarrow[/math] Z(%M), says that M has property Z.
Third step. Let's now specify a property that could not possibly apply to any sentence
Let's define K(%M) = false. Say that K means "heavy". (It could mean anything, really). There is no number or associated sentence that is "heavy" because K always returns false. We just do not want a heavy sentence in our system. Seriously, we are trying to shoehorn the situation here to prevent anything from being provably heavy.
Fourth step. Let's manipulate this property
Take any true sentence S, such as "my cat is sick", because if it is true, then the equivalence:
S [math]\leftrightarrow[/math] not K(%S)
will hold. K(%S) will be false. So, not K(%S) will be true. Hence, that true sentence S is simply not "heavy". The following step is merely syntactic. We negate both sides of the equivalence:
not S [math]\leftrightarrow[/math] not not K(%S)
After simplifying "not not" for canceling each other, we obtain:
not S [math]\leftrightarrow[/math] K(%S)
Since K is always false, we can see that K(%S) = K(%(not S)) = false. Therefore, we are allowed to replace K(%S) by K(%(not S)):
not S [math]\leftrightarrow[/math] K(%(not S))
For the sake of the argument, let's now rename "not S" to "P":
P [math]\leftrightarrow[/math] K(%P)
Look at that! We now have a sentence P that has the property of being heavy, even though K, the heaviness predicate, always returns false! How is that possible?
Fifth step. Conclusion
Well, that is exactly what the Gödel-Carnap lemma says: For each predicate that is computable in natural number arithmetic, there will always be a logic sentence that successfully has that predicate (and also one that successfully does not have it). This cannot be avoided.
Example use of this lemma. Gödel's first incompleteness theorem
It is the necessary existence of the following true sentence (P):
P [math]\leftrightarrow[/math]not provable(%P)
that brought Gödel to fame.
I hope that this explanation is more intuitive than this one. Any comments?
-- disclaimer --
This explanation is just the sketch of an argument by contradiction for the Gödel-Carnap's diagonal lemma, of which the purpose was to give a more intuitive explanation as to why this controversial lemma is provable from number theory. It cannot be considered a fully-fledged proof because it does not implement the complete bureaucracy of formalisms needed in that respect, and also because a complete, original proof by contradiction would need to be thoroughly peer reviewed.
When people write things like this:
The Diagonal Lemma (of Go?del and Carnap) is one of the fundamental results in Mathematical Logic. However, its proof (as presented in textbooks) is very un_intuitive, and a kind of “pulling a rabbit out of a hat”. As a matter of fact, several theorems that are proved by using this lemma now have diagonal-free proofs.
They express their (utter) dislike for this lemma.
Especially its proof is considered to be incomprehensible. That is a problem because both Gödel's first incompleteness theorem and Tarski's undefinability theorem trivially follow from this lemma. Let's attempt to come up with a more intuitive explanation anyway.
First step. We must be able to encode logic sentences as numbers.
Nowadays, doing that is actually trivial. This page is encoded in utf8. It is a perfectly suitable Gödel numbering. We do not need to use Gödel's original encoding which he designed back in the 1930ies before computers existed.
For example, %A = 65 (decimal). That means: the number for the letter A is 65.
Or %(hello) = 0x68656c6c6f (hexadecimal) = 448378203247 (decimal)
You can convert any language expression online from utf8 to hexadecimal (base=16) using this test page and then from hexadecimal to decimal (base=10) using this test page. So, whatever expression we write, in logic or in natural language, we can always represent it as a natural number.
Second step. We must be able to represent properties of logic sentences.
How do we represent the sentence, "The banana is yellow", in logic? If the predicate function yellow is computable and if it accepts a natural number as input, then this form will do the job:
banana [math]\leftrightarrow[/math] yellow(%banana)
It means that the banana has the property yellow. In general, the syntactical form, M [math]\leftrightarrow[/math] Z(%M), says that M has property Z.
Third step. Let's now specify a property that could not possibly apply to any sentence
Let's define K(%M) = false. Say that K means "heavy". (It could mean anything, really). There is no number or associated sentence that is "heavy" because K always returns false. We just do not want a heavy sentence in our system. Seriously, we are trying to shoehorn the situation here to prevent anything from being provably heavy.
Fourth step. Let's manipulate this property
Take any true sentence S, such as "my cat is sick", because if it is true, then the equivalence:
S [math]\leftrightarrow[/math] not K(%S)
will hold. K(%S) will be false. So, not K(%S) will be true. Hence, that true sentence S is simply not "heavy". The following step is merely syntactic. We negate both sides of the equivalence:
not S [math]\leftrightarrow[/math] not not K(%S)
After simplifying "not not" for canceling each other, we obtain:
not S [math]\leftrightarrow[/math] K(%S)
Since K is always false, we can see that K(%S) = K(%(not S)) = false. Therefore, we are allowed to replace K(%S) by K(%(not S)):
not S [math]\leftrightarrow[/math] K(%(not S))
For the sake of the argument, let's now rename "not S" to "P":
P [math]\leftrightarrow[/math] K(%P)
Look at that! We now have a sentence P that has the property of being heavy, even though K, the heaviness predicate, always returns false! How is that possible?
Fifth step. Conclusion
Well, that is exactly what the Gödel-Carnap lemma says: For each predicate that is computable in natural number arithmetic, there will always be a logic sentence that successfully has that predicate (and also one that successfully does not have it). This cannot be avoided.
Example use of this lemma. Gödel's first incompleteness theorem
It is the necessary existence of the following true sentence (P):
P [math]\leftrightarrow[/math]not provable(%P)
that brought Gödel to fame.
I hope that this explanation is more intuitive than this one. Any comments?
-- disclaimer --
This explanation is just the sketch of an argument by contradiction for the Gödel-Carnap's diagonal lemma, of which the purpose was to give a more intuitive explanation as to why this controversial lemma is provable from number theory. It cannot be considered a fully-fledged proof because it does not implement the complete bureaucracy of formalisms needed in that respect, and also because a complete, original proof by contradiction would need to be thoroughly peer reviewed.
Comments (67)
Thanks for this. Just curious, is there a constructive argument for the lemma, such that it also holds for intuitionistic logic where proof by contradiction is not allowed?
Yes, the standard proof does not exploit any contradictions. Its proof strategy is exclusively based on judicious symbol manipulation.
Unfortunately, the standard proof use the original Gödel encoding, which means that it must use two successive encodings/decodings, which is not needed when using a modern numbering scheme. But then again, I guess that tradition has its weight.
What I did was just showing that even in the most extreme case the lemma still holds. In a complete proof it would be a case of formally covering all possibilities. Still, such complete proof would probably no longer be suitable as a clarifying explanation either.
At the Workshop on Proof Theory, Modal Logic and Reflection Principles (October 18, 2017), Moscow, Steklov Mathematical Institute, the speaker was so fed up with the standard proof ("I can never remember it!") that he proceeded by show casing diagonal-free proofs. During the public Q&A, quite a few members of the audience were not convinced about the idea of dropping the diagonal lemma. I actually share that opinion. I think that it is much better to build a better narrative around its proof.
But because prior steps hinged on S = true, it must be the case that this P = not S = false, so as you have presented it at least, we only know that there is some false proposition that has the same truth value as a predicate function that always returns false, which... duh. I don’t see how any conclusions can be drawn from that to more general statements about predicate functions that sometimes return true or sentences that are true. So to get from here to Quoting alcontali
requires either that P be false and “not provable()” always returns false, or else some other step I’m missing. We could trivially invert the truth values and say that any true sentence has any predicate that always returns true, but again, duh, and for that to apply to this situation would require “not provable()” to always return true, which just says that in a system in which nothing is provable, any true sentence is not provable, which is again trivial.
Well, p [math]\leftrightarrow[/math] q also means not p [math]\leftrightarrow[/math] not q, which is indeed a bit "duh", but formally still correct.
Quoting Pfhorrest
My argument just shows an example of an extreme case, really. It is just a case in which you would intuitively not expect the lemma to work, but it still does.
If you want to cover all possible cases, you can always fall back on the full proof. The problem with that full proof is that it is exclusively syntactic symbol manipulation. In the video of the workshop, they pointed out many complaints from people who simply disliked the theorem and its proof for that reason. So, I wanted to show an example where it (unexpectedly) works.
If you provide another example of a class of computable predicates (that return sometimes true and sometimes false) it should also be possible to locate a sentence that will satisfy the lemma.
Quoting Pfhorrest
Well, in that case, you would reasonably expect that every sentence would have the property, which is surprisingly, also not the case. There will still exist a sentence that does not have the property.
Quoting Pfhorrest
Gödel's system will first have loaded all the axioms of logic and all the ones of a (sufficiently strong) theory of arithmetic, and the system understands the full language of first-order logic. Gödel spends dozens of pages doing exactly that in his original paper. The problem is that lots of readers will give up because they consider it to be unreadable (which it actually isn't). Therefore, "nothing is provable" will not occur. You will, for example, be able to prove that "1+1=2".
Then you gave a SKETCH of a proof, which is probably meaningless in its shortened form.
So we don't know what the problem is, and we don't know its solution.
Yet you guys (and perhaps gals) talk about it as if it was as commonplace as the inner tube on a bicycle wheel.
I really, but really would like to know the point you guys (and perhaps gals) are making. Why are we talking abou this? What is the meaningfulness of talking about two somethings none of us understands, and none of us has any comprehension or concept of?
Let me try again.
It is just a game and you must hit the diagonal.
[math] \begin{bmatrix}(false,false) & (true,false) \\ (false,true) & (true,true) \end{bmatrix} [/math]
The first example predicate, "isEven", will return true if a number is even and false if it is odd.
In this game, you can use whatever logic sentence you want, but if it is true, its number must be even. If it is false, then its number must be odd. You must stay on the diagonal!
The diagonal lemma does not tell you how to do that. It only says that it should be possible to find at least one sentence that will successfully hit the diagonal.
So, let's start up a simple search strategy. We generate arbitrary true sentences and convert them to numbers (using their standard utf8 encoding):
1. utf8( 1=1 ) = 496149
2. utf8( 1=1 or 99=99 ) = 49614932111114325757615757
3. utf8( 1=1 or 99=99 or 0=0 ) = 496149321111143257576157573211111432486148 [math]\Leftarrow[/math] BINGO!
Example 3 is true and even. So, it is a solution, i.e. a witness to the lemma. Just for the sake of the argument, let's now try to find an arbitrary false sentence that is odd:
4. utf8( 0=1 ) = 486149 [math]\Leftarrow[/math] BINGO!
Example 4 is false and odd. So, it is also a solution, i.e. a witness to the lemma.
Let's take another example predicate, "isPrime", which will return true if the number is a prime number, and false if it is not.
Well, again, the lemma does not tell you how to conduct your search strategy. It only says that you can always hit the diagonal. It is always possible. Hence, you should always be able to win that game if you try long enough. There is even an obnoxious proof that guarantees it (and that everybody seems to be complaining about).
By the way, you can use the utf8 to decimal test page to convert directly from logic sentence to natural number. Just use the "BigDecimal" box. It works really well.
So, what is the link with Gödel's incompleteness theorem? The "isProvable" predicate works exactly in the same way as the "isEven" or "isPrime" predicates.
So, you can also play this game with the "isProvable" predicate, but the really interesting game is with the "isNotProvable" predicate, because as soon as you win the game by finding a true sentence, you will have a true sentence that also "isNotProvable", and that is considered to be an astonishing result in metalogic and metamathematics.
Quoting god must be atheist
Well, I am just using a trick of collaborative learning here. I try to force myself to give an understandable explanation about a difficult subject to people who do not understand it, because that also improves my own understanding. So, I was rather hoping to hear really "hard" questions that would somehow compel me to solve them.
Of course, all of that requires people who are interested in learning and who will not merely be complaining that they do not understand things.
So, no, you cannot just say, "you do not understand it". That is not how you test someone's understanding. If you really believe that, then you simply do not understand the term "understanding" itself. You simply need to ask a (difficult) question (and then another one, and so on) and then discover that I cannot find the answer, while I should, if I really understood the problem. It is only the inability to solve problems that reveals a lack of understanding.
Hm. A fine explanation you gave me, huh?
1. How do you hit a diagonal? What is the meaning of "hitting a diagonal"? There must be some meaning other than punching my computer screen with my fist.
2.use whatever logic sentence you want, but if it is true, its number must be even. You haven't told us how to determine the number of a sentence. And once you give us the rule to determine the number of a sentence (I imagine it's ordinal numbers, not cardinals), then...
3. What's a "logic sentence"? I imagine "Badly written, explained or described logic puzzles must be sentenced to spend a minimum of two years, maximum of five years, term in prison, and/or fined ten thousand dollars."
4. I searched the opening topic, and there are no examples. I looked at more posts down the page, and they were incomprehensible. Certainly not on the level of a 12-year-old. (I can certify this. I asked my 12-year-old granddaughter to please tell me in English what you said and she revealed her wisdom to me: "Grampa, it's gibberish.")
6. What are you using as predicate? "isEven" is not an expression I understand.
7. If I am too stupid to understand this, please tell me now, outright, so I shall cease and desist, and not bother you with questions.
I don't think you can prove that. But I can disprove this claim by you.
"You do not understand it", "you do not understand it", "you do not understand it", "you do not understand it", "you do not understand it".
There. Four instances of empirical observations of real occurences that deny the truth of your statement.
I am convinced that a 12-year old can understand it. Seriously, I mean this.
Quoting god must be atheist
This first step is the hardest part and it amounts to learning how to use one text box in a particular web page.
I know from experience that 12-year olds can use otherwise very complicated pages in mobile games. This page is much, much easier to learn how to use than what they already know how to use. Furthermore, learning how to use this page is the hardest part in the Gödel game.
Every minute that I spend on this issue, I get more convinced that it can be explained to a 12-year old.
First, you must be able to reach this page: https://onlineutf8tools.com/convert-utf8-to-decimal.
Just copy this link to your browser bar, or click on the link, or whatever. You will need to go there.
The reason is that we are operating in number theory. So, everything you will say in the game has to be a natural number. This is non-negotiable. Still, you can trivially convert every sentence (or sequence of sentences) into just one number.
You first must configure the page correctly. Somewhere in the middle of the page, you will find the heading:
Utf8 to decimal converter examples Click to use
Below that heading you will find three boxes:
Aliens, UTF8 Lottery Balls, and Big Decimal Number
Click in the box "Big Decimal Number".
Now you will see that the page has moved you up again. You can see two boxes at the top of the page: one box on the left, titled utf8, and another box on the right, titled decimal.
Now you can type any sentence in the utf8 box and it will automatically convert everything that you have typed into one big decimal number in the decimal box.
Example:
I am hungry and I want to eat fish
becomes:
733297109321041171101031141213297110100327332119971101163211611132101971163210210511510446
Again, you really need this step, because if you do not convert your sentences into numbers, you cannot use number theory to say anything about your sentences.
Try to do it for the following example sentences:
CIA Whistleblower 'Professionally Tied' To 2020 Candidate
Which should yield:
677365328710410511511610810198108111119101114323980114111102101115115105111110971081081213284105101100393284111325048504832679711010010510097116101
Try also:
The Surge In "Surprise" Medical Bills Bankrupting Americans Can Be Blamed On Private Equity
Which should yield:
84104101328311711410310132731103234831171141121141051151013432771011001059997108326610510810811532669711010711411711211610511010332651091011141059997110115326797110326610132661089710910110032791103280114105118971161013269113117105116121
Copy/paste a few other arbitrary examples by yourself and convert each sentence into a corresponding big decimal number. Once you can do that, the remainder of the game will be much easier to play.
Let me know if it works for you!
-- Note --
Funny, but true, the entire internet happens to be encoded in a Gödel numbering scheme. Every single page is like that! It is not that they consciously "wanted" to do that. It just turned out to be like that.
I like what you're attempting here. The first two steps seem okay to me.
Quoting alcontali
On my view, this is a category mistake. Sentences aren't the sort of things that are or are not heavy, so K(%M) wouldn't be truth-apt.
Quoting alcontali
It can happen when non-truth-apt sentences are treated as truth-apt. Similar to manipulating the liar sentence or "the King of France is bald" sentence.
From your later post:
Quoting alcontali
Nice example. Makes sense to me.
Quoting alcontali
So would this show that some true sentences are not provable, or just that those "true" sentences are problematic in some way, similar to the liar sentence or the above "heavy" sentences?
I am satisfied with this conclusion.
There are for instance imbedded links to pages... were they there yesterday? Or late last night? (Eastern Daylight Savings Time.)
Even this part and the parts preceding it in the opening quote seem brand new to me:
Quoting alcontali
Again, maybe my memory is playing tricks on me. So I ask you, instead of accusing you: did you reword the opening post?
Well, the term "heavy" was probably a bad choice. I couldn't think of a some good predicate, because the literature pretty much never mentions one. It needs to be something calculable true or false about a sentence. The literature typically says something like: "The sentence S has property K". Any idea of what could be a good example for K?
Quoting Andrew M
Well, since "heavy" is just an arbitrary choice, I wouldn't worry about that. As long as you can calculate the property from a number, it should be ok. For example: "the face is green" should probably work better, because a face can be represented as a number, and figuring out that is green, is just a calculation on its bits and bytes. So, the diagonal lemma says that it should always be possible to construct a face that is green, but also one that is not green.
Quoting god must be atheist
No. I stopped drafting it after probably half an hour or so, and then left it like that.
Thanks.
I think either something about the form of the sentence (e.g., HasAnEvenNumberOfLetters) or about the derived Godel number as a number (e.g., your earlier IsEven and IsPrime predicates). IsProvable doesn't seem to meet that criteria since it depends on the meaning of the sentence.
Quoting alcontali
I'm not sure I follow. "heavy" is a predicate in your third step. But "the face is green" is not a predicate. It's fine as a sentence however (with a Godel number).
I guess what I'm having trouble with is step 3 where you're looking for a property that could not possibly apply to any sentence, yet is predicable of it. Perhaps something that is necessarily false? Such as HasZeroLetters (where a valid sentence must have 1 or more letters).
HasAnEvenNumberOfLetters is also just a property of the number associated with the sentence. Instead of converting to decimal, convert to hexadecimal (or just convert back). Example:
utf8( hello ) = 0x68 0x65 0x6c 0x6c 0x6f
Each group of 2 hexadecimal digits represents a byte. So, for "hello" we have 5 bytes, and therefore an odd number of letters. This simple procedure works for digits in the base plane of utf8. For Greek, Chinese, Japanese, Russian characters (and other non-Latin character sets), it represents one letter as two, three, or four bytes. But then again, you know from the first byte (special value), how many other bytes are attached. So, you can then count the letters by counting the groups of bytes.
Since the restriction of the Unicode code-space to 21-bit values in 2003, UTF-8 is defined to encode code points in one to four bytes, depending on the number of significant bits in the numerical value of the code point. The following table shows the structure of the encoding. The x characters are replaced by the bits of the code point. If the number of significant bits is no more than seven, the first line applies; if no more than 11 bits, the second line applies, and so on.
byte number one (represented in binary) indicates the size of the group of bytes:
0xxxxxxx --> 1 byte, 110xxxxx --> 2 bytes, 1110xxxx --> 3 bytes, 11110xxx --> 4 bytes.
So, counting letters in utf8 is just another numbers game.
Quoting Andrew M
It is also just another numbers game. Say that "12>3" is a simple theorem in arithmetic. Then, the following sequence of sentences is one possible proof:
1) 12>3
2) 12-3>3-3
3) 9>0
In 3) we hit axiom 15 in the equivalent axiomatization: i.e. zero is the minimum element.
So, now we convert the theorem to a number:
utf8("12>3")=49506251
utf8("12>3 ; 12-3>3-3 ; 9>0")=495062513259324950455162514551325932576248
So, now we can say that theorem 49506251 is provable because it is associated to another number. 495062513259324950455162514551325932576248, which is its proof. Therefore, the predicate isProvable(49506251) results in true.
What we need to do, to effectively implement a complete solution, is to store and/or compute the set of all possible 2-tuples :
{ (49506251, 49506...32576248), (theorem2, proof2), (theorem3, proof3), (theorem4, proof4), ... }
From there on, the "isProvable" predicate should work fine simply by attempting a look up in this set of tuples and return true, if it can find a proof for the theorem. It is obvious that this is a thought exercise. Gödel did not go on to execute this plan as to effectively implement "isProvable". He would have needed a computer for that in 1931, which did not even exist by them. Furthermore, even then, it is practically not attainable. Still, in an idealized world the "isProvable" predicate can really be implemented. From there on, it will still not be able to avoid hitting the diagonal lemma: there exists a true sentence which "isNotProvable".
Quoting Andrew M
Yes, again, bad example. There is no easy way to attach a truth value to "the face" (a digital image), even if "green" is a calculable predicate about a digital image. In fact, the sentence really has to be sentence in one way or another ...
Cool. No problem with that.
Quoting alcontali
Thanks! Very clear.
Quoting alcontali
Meaning that ideally every true statement has a corresponding proof and every false statement has no corresponding proof (or perhaps a corresponding disproof)?
And is that the diagonal? (i.e., false/not provable, true/provable)
Quoting alcontali
OK, how does this part work?
Quoting Andrew M
Not every true statement but every theorem will have a corresponding proof. A theorem is defined as a sentence that has a corresponding proof. A true statement is a statement that just happens to be logically true. So, false statements will have no corresponding proof, but the lemma guarantees that there will also be true statements that have no corresponding proof. Such lemma-witness statement will be true, but there is no way that you can prove it.
Quoting Andrew M
Quoting Andrew M
In general the diagonal is:
== GENERAL CASE ==
[math] \begin{bmatrix} sentence/hasPropertyX & false & true \\ false & \color{blue}{\boldsymbol{(false,false)}} & (false,true) \\ true & (true,false) & \color{blue}{\boldsymbol{(true,true)}} \end{bmatrix} [/math]
The diagonal lemma's "diagonal" is depicted in blue in the table.
The diagonal lemma says that it is always possible for any arbitrary property about numbers to hit the diagonal. This means that you can always find a true sentence that has the property but also a false sentence that does not have the property.
In logic language, if S is a sentence and P is a property about numbers and %S is the numerical encoding of S then the canonical logic form for that is: S [math]\leftrightarrow[/math] P(%S).
This lemma is provable for all number predicates; not just provability (which is itself also just a number predicate). Gödel's incompleteness theorem is just an application of this diagonal lemma. It just just one particular example of the diagonal lemma:
== SPECIAL EXAMPLE CASE ==
[math] \begin{bmatrix} sentence/\boldsymbol{\color{green}{isNotProvable}} & false & true \\ false & \boldsymbol{(false,false)} & (false,true) \\ true & (true,false) & \color{blue}{\boldsymbol{(true,true)}} \end{bmatrix} [/math]
The general diagonal lemma itself is not considered to be "amazing". It is this one special application of the lemma in the table above, simply by picking propertyX=isNotProvable, that has shaken heaven and earth in 1931.
In my experience, you can develop a good intuition for these theorems by playing the diagonal game a few times more often.
Pick whatever property. Then, generate arbitrary false sentences until you find one that does not have the property. Next, generate true sentences until you find one that does have the property. You win the game as soon as you hit the two boxes of the diagonal.
The sentence "12>3 ; 12-3>3-3 ; 9>0" is a proof of the theorem "12>3". So the sentence "12>3" is both true and provable. It thus hits the diagonal for that sentence and property (in this case, isProvable).
Also, any sentence can be encoded to (and decoded from) a unique natural number (the Godel number).
Quoting alcontali
This is the part I don't understand. How is this proved?
That is exactly the diagonal lemma.
Take any property, e.g. isLargeNumber. Say that isLargeNumber is true for numbers above 10^20, and false for numbers that are smaller.
Now, the diagonal lemma says that you can always find a true sentence for which isLargeNumber is true. You can also always find a false sentence for which isLargeNumber is false.
Forget about Gödel's incompleteness theorem as long as you do not completely grok the diagonal lemma. Make exercises on the lemma, until you thoroughly understand it.
So a very long sentence could have a Godel number above 10^20 (say, "0=0 and 1=1 and ... 10^20=10^20"). And that sentence could be true or false.
But how about the property isNegativeNumber? That property will never be true.
Actually, you caught me on a semantic problem. I should not have called the property "isLargeNumber". I should simply have called it "isLarge" because it becomes a property of the sentence.
Mutatis mutandis, we should deal with the property "isNegative" and not "isNegativeNumber", even though we will calculate it by checking if the number is negative (which is always false for a utf8 decimal).
Let say that S is a false sentence. isNegative(%S) is false, simply because isNegative of any %X is false. So, since they are both false, the expression:
S [math]\leftrightarrow[/math] isNegative(%S)
is on the diagonal, i.e. in the box (false,false). This means that the sentence S has the isNegative property, even though %S is a positive number.
Given the above, it seems that there doesn't have to be a true statement that is not provable. There could instead be a false statement that is provable. So it would be a choice between incompleteness and unsoundness?
I'm also curious about what happens with isFalse. It seems that it will never hit the diagonal. Is that a problem for the diagonal lemma?
Yes, with false statements already hitting the diagonal (false,false) there is no compelling reason why true statements would hit the diagonal in (true,true). It is simply not possible to make isNegative(%S) return true. So, I don't think that (true,true) could ever occur.
Quoting Andrew M
Yes, that is exactly what Gödel concluded. Either the system is incomplete, hitting the diagnal in (true,true) or else it is inconsistent (=unsound), hitting the diagonal in (false,false). Let me check the exact phrasing of this conclusion:
[i]The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers.
The incompleteness theorems apply to formal systems that are of sufficient complexity to express the basic arithmetic of the natural numbers and which are consistent, and effectively axiomatized, these concepts being detailed below.
There are several properties that a formal system may have, including completeness, consistency, and the existence of an effective axiomatization. The incompleteness theorems show that systems which contain a sufficient amount of arithmetic cannot possess all three of these properties.
[/i]
Now, then the commentators argue that standard number theory "seems' to be consistent:
The theory of first order Peano arithmetic seems to be consistent. Assuming this is indeed the case, note that it has an infinite but recursively enumerable set of axioms, and can encode enough arithmetic for the hypotheses of the incompleteness theorem. Thus by the first incompleteness theorem, Peano Arithmetic is not complete.
Therefore, the (false,false) box in the diagonal was originally not "considered" possible (false and provable) because arithmetic was "considered" consistent. This statement became quite questioned, until at some point it was actually "mostly" proven:
[i]In 1958, Gödel published a method for proving the consistency of arithmetic using type theory.[21] In 1936, Gerhard Gentzen gave a proof of the consistency of Peano's axioms, using transfinite induction up to an ordinal called ?0.[22] Gentzen explained: "The aim of the present paper is to prove the consistency of elementary number theory or, rather, to reduce the question of consistency to certain fundamental principles". Gentzen's proof is arguably finitistic, since the transfinite ordinal ?0 can be encoded in terms of finite objects (for example, as a Turing machine describing a suitable order on the integers, or more abstractly as consisting of the finite trees, suitably linearly ordered). Whether or not Gentzen's proof meets the requirements Hilbert envisioned is unclear: there is no generally accepted definition of exactly what is meant by a finitistic proof, and Hilbert himself never gave a precise definition.
The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, relying either on intuition or the acceptance of a consistency proof such as Gentzen's proof. A small number of philosophers and mathematicians, some of whom also advocate ultrafinitism, reject Peano's axioms because accepting the axioms amounts to accepting the infinite collection of natural numbers.[/i]
So, there is not 100% agreement on the idea that Gentzen's proof of the consistency of number theory is actually finitistic, because the natural numbers themselves are an infinite collection.
So, yes, your interpretation is considered correct: Either a (number-theory-including) theory is inconsistent or it is incomplete. They argued for long after Gödel's initial lecture in 1930 over this conclusion, and the matter was barely settled in 1958.
Standard number theory is considered not to be hitting the diagonal in (false,false) (=inconsistent) but in (true,true) (=incomplete) because its consistency proofs have been accepted.
OK, so my understanding is that one sentence that hits (true,true) for isNotProvable is the sentence that asserts that it is itself not provable. How is that expressed as a mathematical sentence?
Also, why is it thought to be true? Is it simply that assuming that it is provable leads to contradiction?
X [math]\leftrightarrow[/math] isNotProvable(%X)
The diagonal lemma does not tell you, however, how to find that true sentence. It only guarantees that it exists.
Quoting Andrew M
Because such true sentence exists. With "isNotProvable" being a number predicate, there is an X that satisfies it. We do not need to actually find this sentence X.
Quoting Andrew M
This true sentence X has the property "isNotProvable". It is not about a contradiction. It is just about the fact that we can define the "isNotProvable" predicate as a number predicate. From there on, there simply exists a true sentence X that satisfies the diagonal lemma.
Searching for such true witness X, requires you to actually construct the "isNotProvable" predicate first. That can, however, only be done as a thought exercise. That is why we do not really search for X. We are already satisfied with the theorem that it must exists.
If no true but unprovable X has been found to satisfy "X ? isNotProvable(%X)", then why should we consider it to be a satisifiable definition?
Also, would "X ? isNotTrue(%X)" be considered a satisifiable definition? I assume not, but that then raises the question of the criteria for judging that a definition is satisfiable.
Anyway, to my knowledge, the trick to Go?del's incompleteness is that it is about semantics. Originally the theorem was formulated in a syntactic variant, which was much more philosophically obvious, but was later refined to semantics, which is to me much more surprising. The theorem tells us that any sufficiently expressive axiomatic system is (ironically) insufficiently expressive to convey its own semantics.
Here is my question. Incompleteness is incurable - i.e. you cannot complete and incomplete axiomatic system by adding axioms. However, our very proof is done in formal logic, and thus provides a new axiomatic system, which embeds the previous one and eliminates the prior incompleteness by means of logical trichotomy - a statement of the original axiomatic system becomes either true, or false, or not provable (but semantically true or false). This new axiomatic system should be incomplete as well. But proving this would require embedding it once more, and reasoning in a similar way. Now, if we take the closure of this process - meaning, if we assume that any statement is provable if it is provable in at least one of the embeddings that define the semantics of the previous axiomatic system, then I speculate that we may be able to explore all embeddings in attempt to prove any statement using gradually expanding method, starting with finite inference steps in the basis axiom system and gradually adding inferences from the meta-systems. The point is - if we find no proof for a statement at all, than we cannot prove that it is semantically true, because it would mean that a proof existed in one of the embeddings, which is a contradiction. Therefore we cannot prove a statement that cannot be proven in this axiomatic system is semantically true, and to the extent of our logical method, this new axiomatic system can never be proven incomplete.
Or am I missing something here. Is there some uncountability involved or will the semantics eventually become inamenable to effective definition.
Edit: I think that I understand the problem now that I wrote it. :) I suspect that the semantics are not "continuous" with respect to the closure operation. The semantics of this new axiomatic system are probably not contained in the union of the embeddings. I can add the axiomatic system for the semantics of the closure to the list of axiomatic systems as well, but I suspect that this list cannot remain a sequence anymore, if I do this continuously.. and my proof method will probably fail.
Edit 2: To think about it - I am not sure whether an axiomatic system with proofs for all true statements of arithmetic exists. The semantic embedding, as I called it. Not for all statements true in its own semantics, just of arithmetic. Now I realize how many gaps I have in my knowledge. :)
How it materializes in practice is rather that we find a statement S, of which we can prove that neither S nor the opposite of S can be proven in theory T (such as the standard theory of arithmetic). So, is this statement true or false? Well, how can you know this, since you cannot prove anything about it? So, in all practical terms, we do not run into true statements that are unprovable, but into undecidable statements. There are lots of witness statements for fundamental undecidability, some of which must indeed be true, but how can we know that?
Quoting Andrew M
The conclusion of Tarski's undefinability theorem is that the "IsNotTrue" predicate is simply not allowed in arithmetic:
[math] \begin{bmatrix} sentence/\boldsymbol{\color{green}{IsNotTrue}} & false & true \\ false & \color{blue}{\boldsymbol{(false,false)}} & (false,true) \\ true & (true,false) & \color{blue}{\boldsymbol{(true,true)}} \end{bmatrix} [/math]
Both slots on the diagonal are poisonous.
The first slot (false,false) means that there exists a false statement that is not "isNotTrue" (meaning, which is true). Hence, that would be a false statement that is true. The second slot (true,true) means that there exists a true statement that "isNotTrue". Hence, that would be a true statement that would be false. Since the diagonal lemma says that there exists a sentence that will hit the diagonal at least in one of both slots, the "isNotTrue" predicate will always lead to the existence of a liar sentence, i.e. an inconsistency.
Therefore, "isNotTrue", "isTrue", "isFalse", and "isNotFalse" cannot be defined as predicates. It is simply not allowed to put them in the table in the green spot. That is the gist of Tarski's undefinability theorem (or truth theorem):
Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1936, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that arithmetical truth cannot be defined in arithmetic.The theorem applies more generally to any sufficiently strong formal system, showing that truth in the standard model of the system cannot be defined within the system. The undefinability theorem is conventionally attributed to Alfred Tarski. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1936 publication of Tarski's work (Murawski 1998). While Gödel never published anything bearing on his independent discovery of undefinability, he did describe it in a 1931 letter to John von Neumann.
The formal statement of Tarski's undefinability theorem is, of course, expressed in terms of the diagonal lemma:
That is, there is no L-formula True(n) such that for every L-formula A, True(g(A)) [math]\leftrightarrow[/math] A holds.
So, there does not exist such number predicate True(%S) because there would always exist exceptions to the proposition that: S [math]\leftrightarrow[/math] True(%S). That would render the entire theory inconsistent.
I think that there are two remarks that are possibly relevant in this context.
First. These "true but unprovable" statements will appear to use as simply undecidable. Indeed, how are we even going to decide that they are "true", if we cannot possibly prove the statement nor disprove its opposite? Hence, the practical qualification will not be "true but unprovable" but "undecidable".
Second. Number theory (by default: Dedekind-Peano) is a sub-theory of set theory (by default: ZFC), meaning that every number-theoretical theorem can be proven in set theory, but not the other way around. Now, there really are number-theoretical theorems that are fundamentally undecidable in number theory (=DP), but provable in the larger set theory (=ZFC):
[i]Undecidable statements provable in larger systems
These are natural mathematical equivalents of the Gödel "true but undecidable" sentence. They can be proved in a larger system which is generally accepted as a valid form of reasoning, but are undecidable in a more limited system such as Peano Arithmetic.
In 1977, Paris and Harrington proved that the Paris–Harrington principle, a version of the infinite Ramsey theorem, is undecidable in (first-order) Peano arithmetic, but can be proved in the stronger system of second-order arithmetic. Kirby and Paris later showed that Goodstein's theorem, a statement about sequences of natural numbers somewhat simpler than the Paris–Harrington principle, is also undecidable in Peano arithmetic.
Kruskal's tree theorem, which has applications in computer science, is also undecidable from Peano arithmetic but provable in set theory. In fact Kruskal's tree theorem (or its finite form) is undecidable in a much stronger system codifying the principles acceptable based on a philosophy of mathematics called predicativism. The related but more general graph minor theorem (2003) has consequences for computational complexity theory.[/i]
Now, we may not have fundamentally stronger theories than set theory (=ZFC). In other words, there may not be such larger theory of which set theory would just be a sub-theory. Therefore, when a theorem is undecidable in set theory, it may even be absolutely undecidable. One reason why we may not go higher nor further than ZFC, is because ZFC is already at the level of Turing-completeness -- can compute everything that is computable and therefore: can represent all knowledge that can be expressed in language. ZFC is possibly even stronger than that:
[i]What is the relationship between ZFC and Turing machine?
In the other direction, a universal Turing machine can be encoded in ZFC, indeed in far weaker theories, such as relatively small fragments of number theory.
...
Suppose, for reductio, that a Turing machine could decide whether the sentence with Gödel number n
is a theorem of ZFC ... Now, by the diagonalization lemma, there would be a Gödel-style sentence ? such that ... Contradiction is immediate. [meaning: ZFC is stronger than Turing-complete][/i]
On the other hand, Turing Completeness is already a seriously constraining limit:
All known laws of physics have consequences that are computable by a series of approximations on a digital computer. A hypothesis called digital physics states that this is no accident because the universe itself is computable on a universal Turing machine. This would imply that no computer more powerful than a universal Turing machine can be built physically.
This does not mean that there are no attempts at increasing the strength of ZFC by adding new axioms. The web is plastered with such attempts.
Still, successfully arguing that a new axiom is independent of the ten existing axioms in ZFC is a non-trivial job, given the strength of ZFC. After that, they still need to successfully prove from this extended system, a theorem that is provably undecidable in ZFC, such as for example the Continuum Hypothesis. That job is certainly not easy ...
Thanks for the response. I'm sorry I couldn't respond earlier.
Quoting alcontali
I couldn't express myself properly, but this is what I meant. I was attempting to construct an axiomatic system, whose undecidable sentences are not amenable to further evaluation by means of metalogic. The idea was to start with incomplete axiomatic system and to import proofs of undecidable statements by continuously adding meta-axioms. There were problems with this approach.
Quoting alcontali
If I understand you correctly, there are axiomatic systems which preserve the truth values of all statements of Peano arithmetic, but make previously undecidable statements decidable? It is a curious fact. So, we don't actually have an axiomatic system yet, in which all statements of Peano arithmetic are decidable?
Quoting alcontali
Just thinking out loud, I wonder whether we would know if ZFC is semantically complete or not, if it were deductively incomplete? And what would be our course of action if we can't know? And on a related note, I wonder whether a theorem with the same quality as Chaitin's constant for Turing machines can be discovered for ZFC - having definite truth value, but no proof in logic or meta-logic.
Quoting alcontali
Yes, I think that it is also intuitive that ZFC cannot be weaker than a universal Turing machine. I also thought that it cannot be stronger. Since non-deterministic Turing machines are computationally equivalent to their deterministic counterpart and should be able to simulate successfully any deductive system. I mean - that was my intuition anyhow.
Quoting alcontali
I have wondered about this. I am not intimately familiar with the hypothesis, but it becomes ever more so obvious that material and abstract sciences are intertwined together. There are some implicit assumptions here, like discrete finite state and determinism. If I recall correctly non-determinism cannot produce more computability. But it can produce more outcomes, and I cannot tell whether this can contribute to nature somehow. Analog or infinite state may be unfeasible, as per QM. The hypothesis does depend on a number of assumptions, but may be true nonetheless.
Thanks again for the response. It is thought provoking.
By the way, there is a problem with the terminology. Decidability is about computability:
Decidability should not be confused with completeness. For example, the theory of algebraically closed fields is decidable but incomplete, whereas the set of all true first-order statements about nonnegative integers in the language with + and × is complete but undecidable. Unfortunately, as a terminological ambiguity, the term "undecidable statement" is sometimes used as a synonym for independent statement.
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer.
While independence is about provability:
In mathematical logic, independence is the unprovability of a sentence from other sentences. A sentence ? is independent of a given first-order theory T if T neither proves nor refutes ?; that is, it is impossible to prove ? from T, and it is also impossible to prove from T that ? is false. Sometimes, ? is said (synonymously) to be undecidable from T; this is not the same meaning of "decidability" as in a decision problem.
There seems to be a preference to use the term "independent" (mathematics) instead of "undecidable" (computer science) for "unprovability" of the statement or its negation. The problem is caused by the fact that these terms emerged from two different domains, but are very related. Given the Curry-Howard Correspondence, undecidability and independence overlap much stronger than suggested by these commentators:
[i]In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
The Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects. If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program.[/i]
The difference between "undecidable" and "independent" seems to depend mostly "on the peculiarities of either formalism" rather than on truly fundamental issues.
The canonical example of a theorem not provable in Peano arithmetic but in ZFC is:
Kruskal's tree theorem, which has applications in computer science, is also undecidable from Peano arithmetic but provable in set theory.
In fact, the commentators below argue that this does not mean that ZFC is "stronger" than PA. The fact that ZFC accepts the theorem while PA doesn't, is rather a trust issue.
Quoting simeonz
I have found the following (formal) thought exercise on exactly this matter. The author calls such encompassing axiomatic system a "provability oracle for Peano arithmetic":
So having a provability oracle for PA or any other consistent formal system that proves some valid arithmetic truths (like ZFC) is equivalent to having a halting oracle, and thus leads to a provability oracle for any other formal system. In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC and all other formal systems. Hee hee.
PA can see everybody else's theorems as Gödel numbers. So, it actually "knows" everything what these other systems know.
Then, I found the following intriguing remark as a comment to the article on the provability oracle for PA:
More powerful formal systems are not more powerful because they know more stuff. They're more powerful because they have more confidence. PA proves that PA+Con(PA) proves Con(PA) (the proof, presumably, is not very long), but PA does not trust PA+Con(PA) to be accurate. ZFC is even more confident - has even fewer models - and so is even stronger. (Maybe it even has no models!)
ZFC is not more powerful than PA because it knows more stuff. In fact, that would not be possible. Such theorem (as well as its proof) would still be a Gödel number which PA can also reach. Therefore, PA actually "knows" all possible theorems (and their proofs) that can be expressed in language. Therefore, it also knows all the axioms and all theorems (including their proofs) of all the other systems. The problem is that PA does not "trust" them.
Therefore, ZFC does not "know" more than PA. It just trusts more. In some ways, that is not really "stronger" or "more powerful". It could just be that ZFC is more gullible.
I think I understand the nuance. There are undecidable deductively complete theories, so claiming that an undecidable statement makes a theory deductively incomplete sounds strange. Saying that the statement is independent from the axioms, purely as a vocabulary, reduces the confusion.
I will also confess - I realized what profound misunderstanding of Gödel's semantic incompleteness I had. I believed that the theorem states that a valid (i.e. true in every model) statement can be independent from the axioms, which indeed would be exciting. Instead, it only states that a satisfiable statement can be independent. (Edit: And that such statement always exists for powerful enough theories.) The Gödel completeness theorem actually states the contrary to my prior understanding. That for first-order theories, validity and provability are the same. What a terrible confusion on my end. :)
Which makes me wonder. Since the semantic incompleteness proof holds for the standard model, what is the "intended" interpretation for other theories. Is there a criterion for a model being standard in general. For example, in denotational semantics of programming languages, a minimal interpretation is the least fixed point of a certain interpretation operator. I wonder, whether this has analogy for model theory. Such as, by using the compactness theorem and gradually building the interpretation domain, by arriving at domain entities using Skolemization or something.
I also couldn't clear up if ZFC is decidable, undecidable, or not yet established. Wikipedia indicates that there are only decidable sublanguages, while a stackexchange answer indicates that ZFC is recursively enumerable, which if mu-recursively enumerable, should mean that ZFC is decidable by Turing machines.
Quoting alcontali
I find the Curry-Howard Correspondence a little strange. I'm sure it makes sense, but likening axioms to a pre-execution invariant and theorems to a post-execution invariant appears complicated. It may have something to do with formal verification processes, but for me, the relationship between proofs and computation appears to be about enumeration of proofs by turing machines in one direction, and the generation of booleans on the Turing tape for the proven theorems after every inference step in the other direction.
Quoting alcontali
After clearing up my error in understanding, hopefully, I am not very surprised. Indeed, because of Gödel's completeness theorem, if a theory were able to prove a statement of PA that PA iteself couldn't, it would have fewer models. The stronger theory would not simply be deductively stronger, but semantically stronger. I was mistakenly excited that a theory with equivalent semantics (one that is expansion of PA) could cure PA's incompleteness. I was hoping that because the new axioms are not statements of PA itself, but their interpretations, they might result in some completely different configuration, without restricting the model space. But this is apparently not the case, at least for first-order logic.
Edit: correction about Gödel's completeness theorem - I used the term unsatisfiability, where I wanted to say not being valid or unsatisfiable (corrected now)
ZFC is subject to the diagonal lemma, and therefore is syntactically incomplete. Hence, it must necessarily have undecidable statements that can be expressed in first-order logic.
Quoting simeonz
Every legitimate answer that is true, has a proof (semantic completeness), but there exist legitimate questions for which an answer cannot be determined (syntactic incompleteness).
Concerning the implications of Gödel's semantic completeness theorem for other systems than Peano arithmetic, we are talking about advanced model theory, which is an enormous subject in itself. I am not sure about the answer, really. I have never looked into it.
Quoting simeonz
In 1958 [Curry] observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment to the typed fragment of a standard model of computation known as combinatory logic.[4]
In order to illustrate this understanding, it is clearly a question of producing good examples of Hilbert calculi as well as good examples of combinator calculi, along with an argument that maps an example in one formalism to an example in the other. It is a lot of work, but it should allow to develop a deeper understanding of the nitty-gritty details of what exactly Curry meant to say.
It is interesting to work on such explanation by examples, but then again, who else would be interested in reading the results? This discussion on the diagonal lemma is probably already more than what many potential readers would want to handle ...
My understanding from the definition was that for a theory to be decidable, it is necessary to have effective enumeration of its theorems, not to have a theorem for every statement or its negation. In that sense, I thought, whether ZFC is decidable is a separate subject matter from its syntactical incompleteness.
Quoting alcontali
I understand, but just to clarify. I wasn't so much curious about Gödel's semantic completeness directly as application with respect to other axiomatic systems, i.e. examples of models that satisfy a statement that is independent of the axioms. I was wondering whether there exists a definition of some kind of "minimal" class of models for every theory. Because, as it stands, I am under the impression that semantic incompleteness says nothing that the syntactic incompleteness and semantic completeness theorems together don't say. If such models were defined and coincided with our "intuitive" definition of interpretation of a theory (similarly to what denotational semantics offers for recursive programs), and Gödel's semantic incompleteness were shown to apply to such models (i.e. they always satisfied a statement that cannot be derived from the axioms), it would make the claim stand on its own.
Quoting alcontali
Absolutely. I will look into it on my own when I have the time. Logic is a past time interest for me, so I have gaps in my understanding at the moment. But I am trying to cure them, a piece at a time.
Thanks for the responses.
[i]Effective axiomatization. A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is a recursively enumerable set (Franzén 2005, p. 112).This means that there is a computer program that, in principle, could enumerate all the theorems of the system without listing any statements that are not theorems. Examples of effectively generated theories include Peano arithmetic and Zermelo–Fraenkel set theory (ZFC).
Completeness. A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms (Smith 2007, p. 24).[/i]
The issue of syntactic completeness only arises in theories that have effective enumeration of its theorems:
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
Hence, only theories with effective axiomatization can possibly be incomplete. Other theories are not even being considered in this context.
There also may be linguistical confusion again. Many internet sources quote undecidability of PA, talking about sentences of PA's language that cannot be evaluated. The point is - sentences of the underlying language, not theorems of the theory, which implies that particular model semantics are involved. Otherwise, sentences that are not theorems (edit: themselves or their negations) don't have definite truth value in first-order theory, as per the completeness theorem. The wikipedia definition of decidability clearly talks about theorems only:
Quoting Wikipedia
Further in the decidability article, it is clearly stated:
Quoting Wikipedia
Thus neither property implies the other. I should mention that I did confuse the issue somewhat, because recursive enumerability (i.e. effective axiomatization, semidecidability) is actually a weaker property, which does not answer negatively for statements not in the theory. Actual decidability requires negative and positive determination by effective method. Semidecidability is defined later in the same article. Even so, however, decidable, but incomplete theories, are also semidecidable, but incomplete ones. Thus, the statement holds that semidecidability does not imply completeness.
Edit: From reading on the web, I see that there is an important caveat. Every recursively enumerably axiomatizable theory is recursively enumerable. And every recursively enumerable syntactically complete theory is decidable. A complete theory may be undecidable, but for "sensible" theories (with effective axiomatization), completeness does imply decidability. So, as you stated, if ZFC were complete it would be decidable. But since it is not, does my original question - if it is decidable or not still stand? (That is, considering that it is effectively axiomatized, if that matters.)
Quoting alcontali
From the definition you quoted, a complete axiomatic theory has a proof for either the statement or its negation. That does not mean that all such proofs or statements can be enumerated by a single effective procedure simultaneously. (PS. According to the previous edit I made, the answer is yes, for the more conventionally axiomatized theories.)
The summary of Gödel's first incompleteness theorem in the introduction to the Wikipedia article (which you quoted) seems to talk about validity ("capable of proving all truths"), which is not trademark of the first theorem, but the second one. And the account differs from the formulation in the body of the article:
Quoting Wikipedia
I reason, that for a statement to lack proof implies that it is not part of the axiomatization consequences. Not that it is part of the axiomatization consequences, but those cosequences cannot be computed.
Edit: Although, it appears that the theorem have been formulated for primitively recursively enumerable axiomatization originally. (According to this stackexchange remark.) According to the summary of one article I found, it appears to admit extension to non-enumerable theories.
And further in the article:
Quoting Wikipedia
This contradicts the summary, by clearly stating that validity is not the subject of the theorem. And finally, the following paragraph shows that the Gödel sentence is merely satisfiable in the standard model, not in every model:
Quoting Wikipedia
Talking about the relationship between syntactic completeness and decidability, I think that there is some definitional ambiguity again. I think that it is sometimes meant to imply a procedure for evaluating (assigning truth value) to all sentences of the language of the theory (which requires syntactic completeness), or procedure that enumerates all statements satisfiable by the standard model (which isn't actually semantic completeness, because all first-order theories are semantically complete, but completeness with respect to a model).
I suspect that ZFC is not decidable, but then again, it really depends on the link between completeness and decidability. If there exists a procedure to solve the proof problem, the proof problem is decidable. That means that the theorem is provable from the theory. In that sense, provability is a decidability problem, because a proof is a procedure.
Quoting Wikipedia
That is actually what they do in the Wikipedia page.
Quoting simeonz
I think that it is the semantic completeness theorem that throws a spanner in the works: For a statement deemed true by the system, some proof must exist within the system. Therefore, the result would be contradictory, unless the truth of the Gödel sentence is evaluated outside the system. In my impression, the Gödel sentence is true in the metasystem but not provable in the system itself. One of the difficulties in this matter is that some reasoning takes place within the system, and some about the system, from outside the system.
I see. Thinking about it, semidecidability I imagine will carry a lot of practical utility for applications like automated theorem proving, even though it doesn't guarantee termination. Decidability is probably more crucial to theoretic analysis.
Quoting alcontali
I actually don't know how the syntactic incompleteness was proven (through the same meta-logical argument as its semantic counterpart or not), but it seems that you shouldn't need a lot of semantics in order to demonstrate that some statement is independent. If the statement's derivation involves circularity (like the Gödel sentence), it should be entirely a deductive property if this circularity can be eliminated or not. But I might be wrong.
I am not familiar enough with Gödel's semantic completeness theorem. The explanation does not contain elaborate examples to illustrate the details of what they are talking about. It would be quite a job to inject examples in the right places.
For example:
But the ring Z of integers, which is not a field, is also a ?f-structure in the same way. In fact, there is no requirement that any of the field axioms hold in a ?f-structure.
A ring is "almost" a field -- it just lacks inverses (it is not closed under division) -- but that's the little I understand of why this ring is still a model (=?f-structure) of a field ... I hope that Wikipedia will manage to better elaborate on this subject.
I am not familiar either, considering that I didn't understand its significance before yesterday. But from what I understand, it essentially states that inference and semantics are equivalent in a first order theory. If the theory knows something, it is true in all models (i.e. true for all interpretations consistent with the axioms), and if something is true in all models, the theory knows it. I don't find this surprising, as it makes intuitive sense. What I find more surprising is that it doesn't hold for higher order logics, as elaborated here:
Quoting Wikipedia
Quoting alcontali
[s]Actually, to my understanding, the signature is not a model, but the "embodied" part of the alphabet for the language of the theory - the rest being variables, quantifiers, logical symbols, are not specific or have no particular meaning. What the article states, if I read it correctly, is that the signature need not incorporate symbols, which taken as abstract mathematical objects, have semantics compatible with the models of the theory. This seems rather vacuous statement, considering that these are just symbols.[/s]
Edit: Thinking about it again, I probably overtrivialized the statement the article makes. It talks about the structure, not just the signature, which would include the interpretation and the domain as well. Considering their examples, you are right. And then indeed, it sounds a little non-sensical. But what they could mean is that an interpretation could assign 0 and 1 to their usual counterparts. And then addition, multiplication and inverses could map to relations that are subsets of Cartesian products of the integer set, but encode rationals using a pairing function. In other words, the article probably states that the function and relation symbols need not be mapped to their standard counterparts for the domain, but merely to functions and relations consistent with the theory.
Just in case pictures help anyone with the wiki proof.
Grateful for notification of errors, or suggestions for further signposting or clarification.
Single pdf here.
No toilet humour intended. :chin:
I think that the idea of "bends" is certainly useful in helping to understand the proof. However, I think that a video with animation would be very useful to illustrate it, i.e. a youtube video or so. In my opinion, the pdf does not provide enough explanation nor visual feedback about the bends, actually.
Going on my to-do list.
:up:
However I thought I'd first attempt my own ELI12 explanation of the diagonal lemma. Any critiques welcome.
Consider the following sentence:
That is an example of a sentence that refers to itself. What Simon purportedly says is the sentence itself and the predicate is Simon says. Notice that the sentence is always true when Simon says it and always false otherwise. If we name the sentence as S, we can express that result as:
Now suppose that the language we're considering doesn't support the word this (as is the case for certain formal languages). However it does support variables and substitutions. We can construct the sentence 'Simon says v' where v is a variable and have v be replaced by the entire quoted sentence. The result would be:
That substitution procedure is called diagonalization. But we have a problem. If Simon says the full sentence (meaning that it's true that Simon says "Simon says 'Simon says v'"), then what the sentence itself asserts is false (since Simon didn't just say "Simon says v"). The problem is that the inner and outer sentences express different ideas. But there is a solution. We can construct the sentence to instead refer to the result of the substitution procedure, i.e., 'Simon says the diagonalization of v'. Diagonalizing that sentence gives:
And now we're done! If Simon says the full sentence, then he is saying the diagonalization of the inner sentence. Which is just what the sentence itself asserts. So the full sentence is the fixed point of the predicate Simon says. It is true if and only if Simon says it. Naming the sentence as S[sub]2[/sub]:
Generalizing the above for any predicate (F) and sentence (X), we get:
Which is the diagonal (fixed point) lemma. (Ignoring Godel numbering to keep it simple.)
From here it is a small step to Tarski's Undefinability Theorem and Godel's Incompleteness Theorems. Just replace the predicate F with IsNotTrue and IsNotProvable respectively and work through the implications.
Quoting alcontali
Yes, in effect the diagonal lemma can generate the Liar sentence, as follows:
Which, in turn, leads to contradiction in the system. However it raises the question as to what it is about the Liar sentence that makes it problematic. As I see it, the deeper reason is that it promises a sentence that can be evaluated as true or false. However instead of delivering on that promise, it merely returns the same sentence which makes the same promise (and therefore entails an endless cycle).
The Truth-Teller ("This sentence is true") is similar in that it also doesn't deliver a sentence that can be evaluated, merely the promise of one. While assuming it to be either true or false doesn't lead to any contradiction, that truth value is arbitrary. Again not particularly useful or informative.
Now consider the Godel sentence which is, in effect:
Unlike the Liar sentence, assuming the Godel sentence is true doesn't lead to contradiction. Whereas assuming the Godel sentence is false does lead to contradiction.
So the usual conclusion is to accept incompleteness - there is at least one sentence in the system that is true but unprovable. Though an alternative conclusion is that the system is complete but inconsistent.
However there is a third alternative. Specifically, the Godel sentence has the same problem as the Liar and Truth-Teller sentences. It promises to deliver a sentence that can be evaluated (such as "12 > 3" which is provable or conversely "12 < 3" which is not provable (or provably false)). But instead of delivering on that promise, it merely returns the same sentence which makes the same promise (and again entails an endless cycle).
The seemingly natural solution would be to exclude Provable(%S) as a primary predicate (as with True(%S), per Tarski) thus preventing the Godel sentence from being generated via the diagonal lemma.
Gödel's theory T is an unholy concoction of pure logic + number theory.
Take for example the sentence S1="Socrates is human". The truth status of this sentence is determined externally. In terms of the number theory in which we are operating, the truth of this sentence is just being axiomatized. It constitutes an axiomatic extension to the system. It has nothing to do with anything that would otherwise be provable from number theory.
Theory T happily supports this type of sentences. Pure logic (as opposed to number theory + logic) does not try to figure out the truth of basic sentences. This information is always axiomatically supplied from outside the system.
The sentence S2="12 > 3" is different. It is a sentence of which we can determine the provability in number theory itself. Its provability is not externally supplied.
True(S) will actually work fine. It is True(%S) that does not work. Funnelling sentences through the number-theoretical module of the system in order to determine their truth is not allowed. However, you are still allowed to funnel it through the pure logic module of the system with True(S).
OK. What I'm suggesting is that an arithmetic sentence could be defined as only being true (or false) if it is, in principle, provable from axioms (or in the case of a false sentence, that its negation is provable). On that premise, the Godel sentence:
would be neither true nor false. To expand:
If the Godel sentence were false then it would be provable. But in a consistent system, only true sentences are provable. Therefore it cannot be false.
Alternatively, if the Godel sentence were true then it would not be provable. But that contradicts the above premise that true sentences are provable. Therefore it cannot be true.
Thus, on the initial premise above, the Godel sentence would not express a proposition. In this way, it would parallel the Liar sentence which is also normally considered neither true nor false. And also the Halting problem, which no program can in principle satisfy.
There is a complicating twist to this.
A theory such as PA can have more than one model. Say that a theory has five models. A sentence could be true in one model but not in the other four models. Semantic completeness means: if a sentence is true in all models of the theory, then the sentence is also provable in the theory.
So, what does it mean that a statement S is true but not provable in theory T? It simply means that theory T has other models than the one you are considering, say, the standard model, and that in at least one of these alternative models, S is blatantly false.
Gödel's incompleteness theorems also imply the existence of non-standard models of arithmetic. The incompleteness theorems show that a particular sentence G, the Gödel sentence of Peano arithmetic, is not provable nor disprovable in Peano arithmetic. By the completeness theorem, this means that G is false in some model of Peano arithmetic.
The standard model of PA is N, the natural numbers.
You can create an example non-standard model for PA by axiomatizing the existence of a transfinite cardinal in PA in addition to N, the natural numbers. From the compactness theorem follows that this non-standard model is still a legitimate model of PA.
Quoting Andrew M
So, no, because such sentence could be true in one model of the theory and false in another. Therefore, true sentences are not necessarily provable. According to semantic completeness, provability means: true in all models of the theory (without exception).
Note:
Objects can only be defined uniquely up to unique isomorphism. So, all these models satisfying PA are isomorphic with the natural numbers, but are not necessarily the natural numbers. These carbon copies of the natural numbers each start at another transfinite cardinal, and start counting up from there.
Everything you claim from the axiomatic PA definition of natural numbers -- for such claim to be provable in PA -- must also hold to be (logically) true for each of these carbon copies of the natural numbers. Otherwise, it will only be true for the original natural numbers, but not provable from their axiomatic definition (i.e. provable from PA).
Quoting alcontali
OK. Does that just mean that non-standard models of Peano arithmetic are inconsistent? Or is there more to it than that?
The next sentence from that Wikipedia entry says:
Can there be an alternative arithmetic model where the Godel sentence is neither true nor false?
And, if so, can such a model be both consistent and complete?
A model cannot be inconsistent. Only a theory could be.
A model in PA is a carbon copy of the natural numbers. It is just a structure, which is a set, such as: 1,2,3, ... along with a collection of operators {+,-,*,/} that operate on that set. structure = two-tuple: (set, operators).
The standard model of PA is ({1,2,3,...},{+,-,*,/})
A theory is a collection of theorems, i.e. sentences about a model. PA is a theory. If PA is true in structure M, then M is a model of PA. If PA does not hold true in M, then it would simply not be a model of PA.
Hence, if non-standard models of PA were inconsistent with PA, they would by definition not be models of PA.
There is no such thing as the consistency of a model. They fit the bill (of the theory) or they don't.
Quoting Andrew M
A theorem S will be unprovable in theory T, if S has a different truth status across T's models. I am not sure that model theory implies that this is the only possible reason for unprovability.
I am not sure about the answer. I am not sure that the existence of nonstandard models is the only source of unprovability/undecidability in PA. This is about the limitations of model theory. This is a hard question!
OK. So, per the earlier Wikipedia quote, what does it mean that the Godel sentence (G) is false in some (non-standard) model of Peano arithmetic? Since that implies that G is provable, isn't that an inconsistency?
Quoting alcontali
I see the issue as similar to the Halting problem. To the question of whether the pathological program halts or loops, the answer is that such a program cannot exist. Similarly, to the question of whether the Godel sentence is true or false, the answer, it seems to me, is that without a process for inferring truth (or falsity), such a sentence cannot be truth-apt. It's simply a pathological sentence like the Liar sentence.
No, ~G would still not be provable, because to that effect G needs to be false in ALL models.
Provability of G means: G is true in ALL models
Provability of ~G means: G is false in ALL models
If it is true in some and false in others, that means: it is not provable nor disprovable in the theory.
Truth is attached to a model. Provability is attached to the theory, which may have more than one model. If a theorem has mixed truth status in the models then it will not be provable or disprovable in the theory.
Example.
Theory T has model M1 and M2.
Sentence Sa is true in M1 and true in M2. Hence, Sa is provable in T.
Sentence Sb is false in M1 and false in M2. Hence, ~Sb is provable in T.
Sentence Sc is true in M1 and false in M2. Hence, Sc is not provable and ~Sc is not provable in T.
What is a theory? A set of rules.
What is a model? A set of objects (with operators on them)
At first glance, PA arithmetic theory, which is a set of rules, describes just the natural numbers. However, that turns out not to be true. There are other sets of numbers that also satisfy the rules of PA. Hence, the natural numbers are considered the "standard" model, while these alternatives that also satisfy these rules, are considered "non-standard" models.
Imagine that you try to describe a car by giving rules which objects must satisfy in order to be considered a car. It must have wheels. It must have a steering wheel. And so on. At this point, the set of Ford vehicles (model 1) satisfy the rules, but also the set of Harley-Davidson motorbikes (model 2).
No matter how precisely you design the rules of PA arithmetic, there will always be other models than the natural numbers that will satisfy these rules. The set of objects described will be unique only up to an isomorphism. Any theory that is complex enough will exhibit the same problem of having multiple models. If a theorem is true in some models but false in other ones, then this theorem will not be provable in the theory. That is the basic idea of model theory.
Working through the logic, G is:
So ~G is:
Now ~G (as with G) is not provable since it can't be derived from the axioms of the theory. Therefore, according to what you've said, ~G (as with G) must be true in some models of the theory and false in others.
However since ~G negates its inner sentence, ~G unpacks further as:
Or, more simply:
If that is correct, then it seems that ~G can't be true in any model of the theory, since G isn't provable.
If, in a nonstandard model, G is false, then ~G is true there.
Is that the same as saying, "If, in a nonstandard model, G is false, then G is provable there"?
No, provability means: true (or false) in ALL models. The lack of provability in theory T is caused by the existence of a mixture of true and false in its models. True in some models and false in others.
What I don't get is why the negation of G shouldn't be interpreted as saying that G is provable. Since G is saying that G is not provable, then it seems to me that to negate G is just to say that G is provable.
We're obviously interpreting ~G differently, but I don't understand how you're interpreting it, nor what you think I'm specifically getting wrong in the above.
Yes, there is a problem there. In a nonstandard model it would say that G is provable, while it isn't. Wikipedia says the following about that problem:
[i]Arithmetic unsoundness for models with ~G true
Assuming that arithmetic is consistent, arithmetic with ~G is also consistent. However, since ~G means that arithmetic is inconsistent, the result will not be ?-consistent (because ~G is false and this violates ?-consistency).[/i]
?-consistency is inconsistency at the level of a combination of universally quantified propositions:
[math]\forall x \in N: K(x) \wedge \exists y \in N: \neg K(y)[/math]
It is different from outright inconsistency:
[math]\exists x \in N: K(x) \wedge \neg K(x)[/math]
Having models with ~G true causes trouble, but does not end up rendering arithmetic inconsistent, only ?-inconsistent.
But we're discussing non-standard models where ~G is true. Since ~G says that G is provable then, if ~G is true, G is provable.
However since G isn't derivable from the axioms of the theory, G is not provable. Therefore there can be no models where ~G is true.
Which would seem to render discussion of models with ~G as true as moot.
There are, and they are arithmetically unsound: Arithmetic unsoundness for models with ~G true.
Quoting alcontali
Consider a non-standard model where ~G is true.
Since ~G says that G is provable then, if ~G is true, G is provable. Now ~G is true (in that model) therefore G is provable (in that model).
It seems you disagree with this. Which part and why?
Concerning "G is provable (in that model)", it should be phrased as "G is provable (in the theory of which M is a model)". Sentences are true or false in a model. Sentences are provable or unprovable in a theory.
Concerning "Arithmetic unsoundness for models with ~G true", the very first remark to make is that the model is unsound. The model contains a sentence ~G as true, while it is false. That is unsound.
Inconsistency, however, means that both ~G and G would be provable from the theory. This is not the case, because neither are provable. Hence, the theory is consistent but one of its models is unsound.
The nonstandard model is indeed unsound but that does not make the theory inconsistent.
Concerning "Since ~G says that G is provable then, if ~G is true, G is provable", no. The model says this, but it simply says something wrong.
G is not provable. ~G is also not provable. Therefore, ~G being true, is simply wrong in the model.
It just means that the model is unsound, meaning, that it contains a statement that of which it says that it is true, while it is actually false.
However that Wikipedia link doesn't provide an external reference and a search on "arithmetic unsoundness" doesn't return anything useful. From my own investigation, it seems instead that ~G being true is understood as correct for non-standard models. See the quotes below.
Quoting Truth of the Gödel sentence - Wikipedia (italics mine)
Quoting 2.6 Incompleteness and Non-standard Models - SEP (italics mine)
Quoting John Baez - professor of mathematics at the University of California, Riverside
That sounds intriguing and intuitively correct, but unfortunately, also difficult to verify, because these nonstandard numbers are infinite cardinalities. So, yes, if there is a proof it will be encoded in one of these infinite cardinalities, which is indeed not a natural number n.
Yes.
So I think there's a lot of baggage that comes along with accepting the Gödel sentence in one's logic system. I suggest that the sentence is not truth-apt.