Dtyjlui

In "Emperor's New Mind", from pages 132 to 141, Roger Penrose explains Gödel's incompleteness theorem in very simple terms. Basically he says that, in a system of ordered propositions ($P_1(w)$, $P_2(w)$, ..., $P_n(w)$) and ordered proofs ($Pi_1$, $Pi_2$, ..., $Pi_n$), the $k$th proposition is $P_k(w) = nexists x [ Pi_x , proves , P_w(w)] $. If we apply $k$ to $Pk(w)$ we will get $P_k(k) = nexists x [ Pi_x , proves , P_k(k) ]$, which is a Gödel-unprovable proposition.

That is a simple explanation, and it makes perfect sense to me, on the other hand Gödel original paper is very complicated, and there are a lot of discussion on the internet on how to understand and how to explain Gödel's theorem to laypeople, which means there is probably some more complicated part of the theorem that is absent of Penrose's explanation. Is that right? What is it?

(Penrose himself says there is a part of Gödel's argument that is super-complicated, but that it is only the part that explains and proves that it is possible to have mathematical proofs and propositions written using only numbers, no symbols -- with some numbers meaning symbols? -- and that these numbers can be operated and ordered like normal numbers, is that the answer to my question above? If yes, how important is this part to the total comprehension of the whole argument? It doesn't seem very important.)

As I am not experienced in these mathematical things, please forgive (and hopefully fix) my mistakes in this question.

A large part of Gödel's paper (see https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf for an English translation) consists of establishing the encoding of the syntax and proof-theoretic notions of a proof system – this is what we now call a Gödel numbering – and of showing that this encoding satisfies certain nice properties.

In particular, Gödel proves that provability within the proof system under consideration can be expressed as an arithmetic function; informally speaking, this makes the formal system able to speak about itself. The technical details are not important for understanding the idea of Gödel's proof, but if one wants to understand why this is at all possible, the technical development is highly important.

In addition to the details involved in constructing the godel-numbering of the formal system, there are two further general points that are missing from the simple description given in the question.

1. The theory of the propositions ($P_1(w)$, $P_2(w)$, ..., $P_n(w)$) needs to be consistent. If this theory is not consistent then any proposition, including $P_k(k)$, is provable from the theory. As this would contradict Godel unprovability consistency needs to be (formalised and) assumed.


2. 
   $P_k(k)$ might be unprovable because $lnot P_k(k)$ is provable. Now $lnot P_k(k) = exists x [ Pi_x , proves , P_k(k) ]$ stating that a proof of $P_k(k)$ exists, a proof whose index is $x$. Ruling this out required the assumption of $omega-$consistency of the given theory (of arithmetic).

In his second book Shadows of the Mind Penrose develops the core Godel argument and examines these two conditions and their relationship to his wider Godel-Turing AI thesis. Both of these conditions, especially the consistency assumption, are seen as a weakness in his argument by some mathematicians and certainly introduce complications.