A How Does Gödel's Diagonalization Relate to Proofs in Peano Arithmetic?

[arupel]

I can readily accept that the Godel sentence The theorem is that "This theorem is not provable" can be expressed in the language of Peanno Arithmetic.

2. Godel on the other side of a correspondence with the above, first translates the Godel sentence using the Godel numbering system

3. Having done this he translated the entire Peanno statement to the Godel numbering system.

This whole statement I think can be called a double diagonalization, in the sense that this is used in this content.

People use the diagonalization of numbers as an analogy to Godel's statement.

1. I cannot understand how translation of the Peanno statement to Godel's numbering system is diagonalization.

2. How does this procedure proves that the Godel sentence is neither provable and not proveable?

Thanks

 

[Demystifier]

2. How does this procedure proves that the Godel sentence is neither provable and not proveable?

It doesn't. Godel theorem states that if peano axioms are consistent, then the Godel sentence is neither provable nor disprovable. But Godel does not prove that the axioms are consistent

 

[stevendaryl]

I have not heard the expression "double diagonalization". But I think I can explain how the Godel sentence is not provable (assuming that the axioms are all true of the natural numbers).

Let's call a formula having one free variable, a "property". For example, "x+x=x*x" is a property. You can think of a property as an infinite vector of values, each value being either "true" or "false". So for example, "x+x=x*x" is the infinite vector [true, false, true, false, false, false, false, ...], because it's true when x=0, false when x=1, true when x=2, and false for every other nonnegative integer.

Now, imagine listing all possible properties definable in the language of arithmetic. You can think of this as an infinite two-dimensional matrix T(n,m), where entry number (n,m) is "true" if property number n holds for value m.

For Godel's purposes, we are interested in what's provable, rather than what's true. So let H(n,m) be the two-place predicate meaning "It is provable that property number n holds of value number m". So H is a different infinite two-dimensional matrix, except that element number (n,m) is only true if the corresponding element of matrix T is provable. Note that there are two possible differences between H and T. Something could be true, but not provable. Or something could be provable, but not true (if your axioms are wrong, for instance).

Here's where the diagonalization comes in: If you think of H as an infinite two-dimensional matrix, then the "diagonal" of the matrix consists of the elements with label (n,n). So let D(x) be the property "H(x,x)". D(n) is true if and only if it is provable that value number n holds of property number n. So for example, if property number 27 is "x+2=29", then substituting 27 in for "x" in property number 27 results in a provably true statement, "27+2=29". So in that case, D(27) would be true.

The next twist is to negate D(x). Let G_0(x) be the formula \neg D(x). This is yet another property. If property number 42 is "x+1=2", then substituting 42 for x in property number 42 is the statement 42 + 1 = 2, which is false. Presumably, we've constructed our axioms so that you can't prove false statements, so there should be no proof of this statement. So D(42) is false. Since G_0(42) is the negation, then G_0(42) will be true.

The final twist is to note that G_0 is itself a property definable in arithmetic, so it has a number, say 2017 (it would probably be much, much larger). Now, let's look at the statement G \equiv G_0(2017).

Now, G is some statement of arithmetic. Is it true? Well, let's unravel it. If it's true, that means that G_0(2017) is true, but by definition of G_0, that means that D(2017) is false (since G_0 is the negation of D). But look at the definition of D: D(2017) is true if it is provable that property number 2017 holds of value number 2017. But property number 2017 is G_0. So D(2017) is true if it is provable that G_0(2017) holds. Since G_0 is the negation of D, we have:

G_0(2017) is true if it is not provable that G_0(2017) holds. So in terms of G \equiv G_0(2017):

G is true if and only if G is not provable.

So there are two possibilities:

1. G is true, and it is not provable.
2. G is false, and it is provable.

If our axioms are sound (they don't allow us to prove anything false), then possibility number 2 is ruled out, so the conclusion is that G is not provable.

 

[SSequence]

As someone without a technical understanding of these theorems, here are few basic qualitative questions.

Lets denote the formal system involved by F. I am assuming that following statements are equivalent(?) :
Statement S is provable in F == Statement S is true in F
Statement S is disprovable in F == Statement S is false in F

So there are two possibilities:

1. G is true, and it is not provable.
2. G is false, and it is provable.

If our axioms are sound (they don't allow us to prove anything false), then possibility number 2 is ruled out, so the conclusion is that G is not provable.

This makes sense if we assume that F is sound. However, that seems to be a much more strict condition than consistency of F (which seems to be the assumption in both the theorems).

-----

Also a question about second theorem. For a consistent system F, we construct a specific statement asserting consistency of F (call this statement S). According to second theorem, if F is consistent then S can't be true in F.

Does the second theorem also preclude the possibility (assuming F to be consistent) that S can't be false in F ... or it doesn't preclude that possibility? And if it did preclude that possibility, wouldn't that mean that the first theorem follows trivially from the second?
But even if the second theorem doesn't preclude this possibility, wouldn't it be fair to say that on the very least it proves: "If F is sound then F is incomplete."?

What I sort of meant was that assume F really is consistent. However, if it the statement ~S(complement of S above) asserting "F is inconsistent" was true in F, then this just makes the system F definitely unsound but not necessarily inconsistent? So can the truth of statement ~S be allowed in F? Or is this possibility just too silly -_-

edit: The idea I had roughly in mind with the second question was that given some system F we often add the statement S (asserting consistent of F) to it to form the system F1=F+{S}. However, if we want to be sure that F1 itself is consistent (even assuming that F was consistent) then shouldn't we also be able to show that ~S was never proved to be true in F?

p.s. My head is spinning after writing the second question :p. Hopefully it makes some sense.

 

[stevendaryl]

As someone without a technical understanding of these theorems, here are few basic qualitative questions.

Lets denote the formal system involved by F. I am assuming that following statements are equivalent(?) :
Statement S is provable in F == Statement S is true in F
Statement S is disprovable in F == Statement S is false in F

No, those are not the same. Provable is relative to a set of axioms, while truth is relative to an intended interpretation of the sentence.

Some sentences don't necessarily have an intended interpretation, in which case, there is no notion of "truth". But in a case such as arithmetic, there is an intended interpretation of sentences.

There are three ways that provability can be different than truth:

1. There is no intended interpretation of the sentences, so there is no notion of truth.
2. The axioms are too weak to prove all the true statements, so there are true statements that are not provable.
3. The axioms are just wrong (for the intended interpretation), so you can actually prove things that are false.

This makes sense if we assume that F is sound. However, that seems to be a much more strict condition than consistency of F (which seems to be the assumption in both the theorems).

What you can show is that:

• If F is consistent, then G is not provable by F.
• If F is sound (only proves true statements), then G is not disprovable by F, either.

If F is only consistent, but not sound, then it's possible that F proves \neg G.

Also a question about second theorem. For a consistent system F, we construct a specific statement asserting consistency of F (call this statement S). According to second theorem, if F is consistent then S can't be true in F.

No: If F is consistent, then there is no proof of S. S might still be true. (and will be)

Does the second theorem also preclude the possibility (assuming F to be consistent) that S can't be false in F ... or it doesn't preclude that possibility? And if it did preclude that possibility, wouldn't that mean that the first theorem follows trivially from the second?

The second theorem says that if F is consistent, then F cannot prove that it is consistent. It follows from the first theorem:

• G is true if and only if F is consistent
• So if you can prove F is consistent, then you can prove G.
• So if F can prove "F is consistent", then F can prove G.
• But if F is consistent, then F cannot prove G.
• Therefore, if F is consistent, then F cannot prove "F is consistent"

It's still possible that F proves \neg G, if F is unsound. In that case, F can be consistent, but can prove the false statement "F is not consistent".

 

[SSequence]

No, those are not the same. Provable is relative to a set of axioms, while truth is relative to an intended interpretation of the sentence.

I think there might be confusion w.r.t. terminology perhaps? When I said "S is true in F", I simply meant something along the line of "at some point while writing about truth of statements (well-defined in F) the system F will declare S to be true". In no way I was referring about "actual" truth value of S anywhere (whether that is evidently easy to define or not is another matter).

To keep things as simple as possible, let's assume that F only asserts statements to be true (and not false). What I meant more fully was:
(1) S is provable in F: At some point F will assert S to be true
(2) S is disprovable in F: At some point F will assert ~S to be true
(3) S is neither provable nor disprovable: F never asserts anything about S or ~S being true

The statements (1) and (2) can also be read as:
S is true in F
S is false in F

As for your second sentence, since I am not aware of any details of model theory at all, I would ask do we have to bring "interpretation" at all costs even for very simple systems? Even for simple kind of number theoretic statements that lie in a certain limited domain?

No: If F is consistent, then there is no proof of S. S might still be true. (and will be)

I was saying exactly the same thing that you said (maybe my wording isn't standard or clear enough). When I said "S can't be true in F", I meant that F will never assert S to be true. This is the same as saying F doesn't have any proof of S.

What you can show is that:

• If F is consistent, then G is not provable by F.
• If F is sound (only proves true statements), then G is not disprovable by F, either.

If F is only consistent, but not sound, then it's possible that F proves \neg G.

My question is/was that doesn't this only show "If F is sound then F is incomplete"?

If F is consistent and it possibly proves ~G, then how does this say that F is incomplete? Wouldn't incomplete mean that there is some statement S for which F asserted neither the truth of S nor the truth of ~S. If it asserted anyone of the two then the statement S shouldn't be sufficient to say F is incomplete.
Wouldn't the argument need to be modified in some way for this more general case?

Also what about the statement:
wouldn't it be fair to say that on the very least second theorem proves that: "If F is sound then F is incomplete."?edit: Have to read the last part of your post yet.
Made a few modifications in the post.

Edit:
Read the last part of your post. I couldn't follow your reasoning but you wrote in the end:
"F can be consistent, but can prove the false statement "F is not consistent"."
If indeed that is true then when I wrote in previous post (S here being some definite statement that says "F is consistent"):
"edit: The idea I had roughly in mind with the second question was that given some system F we often add the statement S (asserting consistent of F) to it to form the system F1=F+{S}. However, if we want to be sure that F1 itself is consistent (even assuming that F was consistent) then shouldn't we also show that ~S was never proved to be true in F?"
So does this mean that if we want to make sure that F1 is consistent then we have to show both of the following(?):
i) Make sure F is consistent.
ii) Make sure ~S is never asserted as true in F.

I think one might also have to realize in that case that we are just talking about one specific statement S asserting consistency of F. There might be some another statement S2(not the same as S) that also asserts "F is consistent". And it might be possible then that while, F is consistent ... and never asserts ~S as true, it still does assert ~S2 as true. In that case, both F and F1 will consistent but both will be unsound.

 

[stevendaryl]

My question is/was that doesn't this only show "If F is sound then F is incomplete"?

Right, that's what Godel's original theorem proved. That left open the possibility that F might be unsound and complete. A slight generalization of Godel's proof (I can't remember who proved it) shows that if F is consistent, it must be incomplete (whether or not it is sound).

Instead of contstructing a sentence:

G \leftrightarrow G is not provable.

you construct a sentence

Q \leftrightarrow "if there is a proof of Q, then there is an even shorter proof of \neg Q"

If Q is provable, then you can check all shorter proofs to see if there is a proof of \neg Q. If there is, then you have a contradiction. If there is not, then what Q says is false, so Q is provably false, and also provably true. So F is inconsistent.

On the other hand, if \neg Q is provable, that means that there is a proof of "There is a proof of Q and there is no shorter proof of \neg Q" (the negation of "if A then B" is "A and not B"). So again, you can check all the proofs shorter than your proof of \neg Q to see if any of them prove Q. If so, you have a contradiction. If not, you have a different contradiction.

So if F is consistent (not necessarily sound), then neither Q nor \neg Q is provable.

 

[SSequence]

Right, that's what Godel's original theorem proved. That left open the possibility that F might be unsound and complete. A slight generalization of Godel's proof (I can't remember who proved it) shows that if F is consistent, it must be incomplete (whether or not it is sound).

Alright that makes things clearer. I haven't read the extended argument you wrote yet though.

But it is a bit strange that in that case the first theorem essentially can be seen as corollary to the second one. Because if we state the second theorem as:
S -- some specific constructed statement saying that F is consistent

Second Theorem: "If F is consistent then S can't be proved in F."

Now if we take the assumption that:
i) F is sound
ii) It follows from (i) that F is consistent.
iii) It follows from (ii), using second theorem, that S can't be proved in F
iv) It follows from (ii) that S is true
v) It follows from (iii) and (iv) that F is incomplete.

Hence F is sound implies F is incomplete.

 

[SSequence]

I can't edit the previous post. Here is a minor point.

v) It follows from (iii) and (iv) that F is incomplete.

This would be better written as:
v) It follows from (i), (iii) and (iv) that F is incomplete.

 

[stevendaryl]

Alright that makes things clearer. I haven't read the extended argument you wrote yet though.

But it is a bit strange that in that case the first theorem essentially can be seen as corollary to the second one. Because if we state the second theorem as:
S -- some specific constructed statement saying that F is consistent

Second Theorem: "If F is consistent then S can't be proved in F."

Now if we take the assumption that:
i) F is sound
ii) It follows from (i) that F is consistent.
iii) It follows from (ii), using second theorem, that S can't be proved in F
iv) It follows from (ii) that S is true
v) It follows from (iii) and (iv) that F is incomplete.

Hence F is sound implies F is incomplete.

That's true, but the first theorem is used in the proof of the second theorem.

Basically, the first theorem shows:

"If F is consistent, then F does not prove G"

(where G is a sentence such that G is true if and only if G is not provable in F).

It follows that if F proves "F is consistent", then F proves "F does not prove G". But F also proves [item]G \leftrightarrow[/itex] "F does not prove G". So if F proves "F does not prove G", then F can prove G. But if F can prove G, then F is inconsistent. So we conclude:

If F proves "F is consistent", then F is inconsistent.

That's the second theorem.

 

[SSequence]

What you can show is that:

• If F is consistent, then G is not provable by F.
• If F is sound (only proves true statements), then G is not disprovable by F, either.

I have been thinking about this specific part and I can see the second statement to be true but I am having some trouble having seeing how the first statement has to be true.

Here is, for example, how I see the second statement:
"If F is sound then G is neither provable nor disprovable by F."

(a) G asserted by F (Yes) -- ~G asserted by F (Yes)
(b) G asserted by F (Yes) -- ~G asserted by F (No)
(c) G asserted by F (No) -- ~G asserted by F (Yes)
(d) G asserted by F (No) -- ~G asserted by F (No)

G(true) -- G is not provable in F
G(false) -- G is provable in F

G(true) -- corresponds to possibilities (c) and (d)
G(false) -- corresponds to possibilities (a) and (b)

S(true) -- F is sound
S(false) -- F is not sound

Assume S to be true

Possibilities:
G(true)

possibility (c)
F asserts ~G
F is not sound (G is true and F asserts ~G)
contradiction

possibility (d)
F asserts neither G nor ~G
"allowed"

G(false)

possibility (a)
F asserts G
F asserts ~G
F is not sound
contradiction

possibility (b)
F asserts G
F is not sound (G is false and F asserts G)
contradiction

==========

Now if we look at the first statement:
"If F is consistent, then G is not provable by F."
Similar to above we define:
C(true) -- F is consistent
C(false) -- F is not consistent

Once again, now we assume C (instead of S) to be true and see which possibilities can be ruled out easily. Now if this statement is true, we should able to rule out both the possibilities (a) and (b), right? Well possibility (a) is ruled out in an elementary manner. However, I can't quite see why one can rule out possibility (b) in an elementary manner.
Perhaps I am making a simple mistake or missing something obvious. Or perhaps ruling out this possibility can't be done with qualitative arguments like these. I don't really know to be fair.

 

[stevendaryl]

I have been thinking about this specific part and I can see the second statement to be true but I am having some trouble having seeing how the first statement has to be true.

By construction:
G \leftrightarrow "G is not provable by F"

So if F proves G, then F proves "G is not provable by F".

On the other hand, if F proves G, then it's provable that F proves G.

So if F proves G, then F proves "G is not provable by F", and it also proves "G is provable by F".

 

[SSequence]

I think I have "sort of" got it. For example, here is how I would write it:

"If F is consistent, then G is not provable by F."
(a) G asserted by F (Yes) -- ~G asserted by F (Yes)
(b) G asserted by F (Yes) -- ~G asserted by F (No)
(c) G asserted by F (No) -- ~G asserted by F (Yes)
(d) G asserted by F (No) -- ~G asserted by F (No)

G(true) -- G is not provable in F
G(false) -- G is provable in F
G(true) -- corresponds to possibilities (c) and (d)
G(false) -- corresponds to possibilities (a) and (b)

C(true) -- F is consistent
C(false) -- F is not consistent

Assume C to be true:
G(false)

possibility (a)
F asserts G
F asserts ~G
F is not consistent
C is false
contradiction

possibility (b)
F asserts G
F asserts (F doesn't assert G) // by definition of G

F asserts ~G
F asserts (F asserts G) // by definition of G

If we denote proposition p as:
F asserts G //p true for (a),(b) and false for (c),(d)
then:
F asserts ~p
F asserts p

F is not consistent
Hence C is false
contradiction

==========

That also means that if F is consistent then G is true.

 

[stevendaryl]

There is a fact about provability that is used:

If F proves X, then F proves "F proves X".

So if F proves G, then F proves "F proves G". By construction of G, "F proves G" is the same as "not-G".

 

[SSequence]

There is a fact about provability that is used:

If F proves X, then F proves "F proves X".

I am assuming truth of this implication "only" requires F to be powerful/expressive enough (and nothing more)? For our purposes, for example, on the very least we want this implication to be true for a consistent F (its truth for just a sound F wouldn't suffice for example).

Also, in case you want to answer, what about the reverse implication? That is, would its truth require any conditions on F or not? It seems that on the very least the reverse implication should be true for a sound F.Given this, it makes sense mechanically. Possibility (b) from post#13 (I can't edit the mistake there) can be written simply as:
possibility (b)
F asserts G
F asserts (F asserts G)
F asserts ~G //definition of G

F is not consistent
contradiction