I've been exploring Godel's original 1931 paper On Formally Undecidable Propositions of Principia Mathematica and Related Systems (I'm using an English-translated version found here). And to pre-empt any comments, I'm well aware that there's much clearer explanations for modern readers out there, but I'm curious to see how the result looked in its original form 🙂
I'm particularly curious to find the original G̦del sentence Рi.e., the "I am unprovable" expression that you hear so much about when studying this result.
It seems to me that the Godel sentence is defined on page 188 of his paper (page 61 in the PDF I linked above), section 13, and, with a bit of reorganization, would be
$$
17\;\text{Gen}\;r = Sb\left(p {19 \atop Z(p)} \right)
$$
However, this paper is so dense and has such unfamiliar notation, that it's hard to feel confident in this РI'd love a confirmation that this is the closest thing to the original G̦del sentence.
Best Answer
You are right.
Long comment (very informal):
Gödel's 1931 construction, with respect to a specified formal system $K$, uses predicate $\text B_K (y,x)$ [page 55 of the translation] that reads "$y$ codes a proof in $K$ of formula coded by $x$" and then $\text {Bew}(x) = \exists y \text B_K (y,x)$ that reads: "there is a proof of $x$", i.e. "$x$ is provable in $K$".
With them [page 58] he defines:
that amounts to saying that "$x$ is not a proof of a certain formula ..." [the author uses the two first variables in the list of the alphabet (call them $x$ and $y$), coded with $17$ and $19$ respectively.]
Using repeated substitutions, a process now called "diagonalization", we arrive at the formula $17 \text {Gen}(r)$, that is $\forall x r(x)$.
If we go back to the steps used to define it, we arrive at something like:
that is equivalent to $\lnot \exists x \text B_K(x, \ldots)$, that reads that there is no code of a proof of a certain formula, that means that that formula has no proof in $K$.
Then Gödel shows, under the assumptions of the main Theorem VI, that both $17 \text {Gen} r$, i.e. $\forall x r(x)$, and $\text {Neg}(17 \text {Gen}r)$, i.e. $\lnot \forall x r(x)$, are underivable in the system $K$, that give us the fundamental result that the formula $17 \text {Gen} r$ is undecidable in $K$.
But, due to the construction sketched above, formula $17 \text {Gen} r$, i.e. $\forall x \lnot \text B_K(x, \ldots)$, reads: