For each consistent formal theory T having the required small amount of number theory, the corresponding Gödel sentence G asserts: "G cannot be proved within the theory T". This interpretation of G leads to the following informal analysis. If G were provable under the axioms and rules of inference of T, then T would have a theorem, G, which effectively contradicts itself, and thus the theory T would be inconsistent. This means that if the theory T is consistent then G cannot be proved within it, and so the theory T is incomplete. Moreover, the claim G makes about its own unprovability is correct. In this sense G is not only unprovable but true, and provability-within-the-theory-T is not the same as truth. This informal analysis can be formalized to make a rigorous proof of the incompleteness theorem, as described in the section "Proof sketch for the first theorem" below. The formal proof reveals exactly the hypotheses required for the theory T in order for the self-contradictory nature of G to lead to a genuine contradiction.

I found this text on Gödel's first incompleteness theorem on wikipedia. I don't understand the statement which states: "If G is provable, then G contradicts itself". Can anyone please elaborate?

P.S: I am new to discussing philosophy. So, I apologize for any mistakes.

We have to recall the statement of the Theorem :

First incompleteness theorem (Gödel). Any ω-consistent formal system S within which a "certain amount" of elementary arithmetic can be carried out is incomplete with regard to statements of elementary arithmetic : i.e.there are such statements which can neither be proved, nor disproved in S.

The argument of Gödel's first incompleteness theorem is a little bit complex.

In addition, the condition of ω-consistency is a little bit "convoluted"; thus starting from Wiki's exposition, we will develop a "simple" argument, assuming the soundness of the system S [i.e.the system S does not prove false sentences; by the way, soundness implies consistency].

1) Arithmetization of syntax :The main problem [is] to construct a statement p that is equivalent to " p cannot be proved" [...] Gödel's ingenious technique is to show that statements can be matched with numbers (often called the arithmetization of syntax in such a way that "proving a statement" can be replaced with "testing whether a number has a given property" [here we need the property of system S to include a "certain amount" of arithmetic: the system S must have enough capabilities in order to "express" the syntactic relations and properties of the system itself].

2) Construction of a statement about "provability" : Having shown that in principle the system can indirectly make statements about provability, by analyzing properties of those numbers representing statements it is now possible to show how to create a statement that actually does this.

Therefore there is a statement form Bew(y) that uses this arithmetical relation to state that a Gödel number of a proof of y exists:

Bew(y) = ∃ x ( y is the Gödel number of a formula and x is the Gödel number of a proof [in S] of the formula encoded by y).

Last step is :

Diagonalization : The next step in the proof is to obtain a statement that says it is unprovable. Although Gödel constructed this statement directly, the existence of at least one such statement follows from the diagonal lemma, which says that for any sufficiently strong formal system and any statement form F there is a statement p such that the system [S] proves :

p ↔ F(G(p)).

By letting F be the negation of Bew(x), we obtain the theorem

p ↔ ~Bew(G(p)),

and the p defined by this roughly states that its own Gödel number is the Gödel number of an unprovable formula.

The statement p [...] states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement. But when this calculation is performed, the resulting Gödel number turns out to be the Gödel number of p itself.

Now we can put all the ingredients together.

The reasoning in Gödel's proof is now as follows. First, if p is in fact a theorem of S, then it is provable in S that p is a theorem of S [that is : Bew(G(p)), the formula which asserts that there exists a number x which is the Gödel number of a proof in S of the formula encoded by G(p)].

The reason for this is that "being a theorem of S" is a property that can be verified by exhibiting a proof in S, and since being a proof in S is required to be a computable property of sequences of sentences, the verification can be carried out within S itself [again : S includes a "certain amount" of arithmetic ...].

Thus, if S proves p, i.e. if p is a theorem of S, then S proves also ~Bew(G(p)), by the equivalence above [recall that p is a provable fixpoint of the property of not being a theorem of S]; but it proves also Bew(G(p)), by the previous argument. So we have a contradiction.

Now consider the case that S proves ~p; by "construction" of p, it proves a sentences "saying that" p is unprovable. Now, we have two possibility .

(i) the proof of p exists : in which case S is clearly inconsistent;

otherwise :

(ii) the proof of p does not exists : in which case S proves a false sentence, because it proves Bew(G(p)), which assert that the proof exists. Thus, S must be unsound.

Conclusion: assuming that S is "capable" of expressing a "certain amount" of arithmetic, the system S cannot be both sound and complete.

But we stay with our "natural insight" about the soundness of arithmetic. Thus, a system "containing" arithmetic must be incomplete.

Having proved that the Gödel's sentence p is unprovable in S, due to the fact that p can be "read" as asserting its own unprovability, Gödel's proof shows that p is true. Thus, in addition to proving the existence of an unporvable sentence, Gödel's proof gives us a method to "manufacture" :

a true sentence expressible in S that is not provable in S.

See Torkel Franzén, Gödel's theorem An incomplete guide to its use and abuse (2005).

If you appreciate how formal systems work in logic and mathematics then Godels theorems are best exposited by taking a detour through a modal logic called provability logic.

There is a (standard) modal logic called K, after Kripke which (standardly) models neccessity, and whose axioms are

1. If T |- p then T |- Np

2. Given T |- N(p -> q) then T |- Np -> Nq

3. For all p, we have T |-Np ->NNp

The first axiom says if p is the case, then p is necessarily the case; then second says if it is neccessarily the case that p implies q, then it is necessarily the case that p neccesarily implies q.

One also notes that if p is neccesarily the case then p is necessarily, necessarily the case, or in symbols it is the third axiom.

We add in a new axiom, whose motivation comes from provability, called Lobs axiom, and which says

Lob: For every p, we have that N(Np ->p) -> Np

In this modal logic we can show that it satisfies a fixed point theorem which says, if given a predicate A(p) depending on a propositional variable p, then there is a formula q in which p does not appear, and

Thm: |- q <-> A(q)

Now, it turns out the provability predicate P in arithmetic satisfies the axioms of the modal logic elaborated above, and so has this fixed point theorem.

Finally, by setting A(p):= not Pp, so saying p is not provable, then its fixed point is not P(_|_), that is it doesn't prove a contradiction, and we have from the fixed point theorem, the sentence:

|- not P(_|_) <-> not P(not P(_|_))

Reading this (from left to right), it says, if we cannot derive an inconsistency, then we cannot prove we can derive an inconsistency. This is Godels incompleteness theorem, which says that a consistent theory has a sentence that is true but unprovable - and we've shown that this statement is contradictions are not proveable.

All this is in the SEP article on provability logic

• I suppose that the last formula must be : ⊢ ¬P(⊥) ↔ ¬P(¬P(⊥)) . Your last comment is - strictly speaking - a paraphrase of G's Second Incompleteness Th. Apr 16 '14 at 8:58
• Yes, you're right! I've fixed it. Sure, but for Godels first theorem don't we need to exhibit a true sentence that is unprovable? Doesn't the sentence ¬P(⊥) fit the bill? since if it is true we have ¬P(¬P(⊥)) which says that this sentence is not provable? Apr 16 '14 at 9:09
• Yes; but this fixpoint says more: it says that the system (if consistent) cannot prove its own consistency; and this is 2nd Th. Apr 16 '14 at 9:46

The only time a system can prove itself true is when that system is contradictory. In those cases the system can prove anything even its own truth and consistency. So if G is provable it's provable because G is contradictory.

G: "G cannot be proved within the theory T"

"If G is provable, then G contradicts itself"

So suppose that someone goes on an manages to prove that G is true within T theory.

But since G states the opposite, ie, that it cannot be proved within T theory, if it is proved true, it is proven... false. So it is contradictory, as it is simultaneously true and false.

It is a variant of the Epimenides paradhox ("Everything that I say is a lie...", which is true only if it is untrue).

Gödel managed to construct a sentence G that expresses "there is no proof for the sentence G". Now look at the sentence that gives you a problem: "If G is provable, then G contradicts itself".

G makes a statement. If the opposite of the statement that G makes is true, then clearly G is false. What is the statement of G? "There is no proof for the sentence G". What is the opposite of that statement? "There is a proof for the sentence G". Earlier we saw "If the opposite of the statement that G makes is true, then G is false". So "if there is a proof for the sentence G then G is false".