why Gödel use $[R(n);n]$ in his introduction?

Question

in "on formally undecidable propositions of principia mathematica and related systems"'s introduction, Gödel used the notation $R(n)$ and $[R(n); n]$ to state the unprovable formula meaning "I am unprovable."

but why he use the notation and don't use directly the statement "I am unprovable"?

if we use the steps to convert from the expression to the class-expression, then really is it converted from metamathematical expression to object-language expression?

and what does it mean that class-expression $[R(n);n]$?

why he didn't use $[R(n);q]$ but used $[R(q);q]$?

(or why we have to use that form?)

How can $\overline{Bew}[R(q);q]$ mean "I am unprovable?"?

Answer 1

"Class sign" means a formula with one free variable [see English translation, page 598].

Formulas are expressions of a formal language (in the original G's article that of Principia Mathematica): the statement "I am unprovable" is not such a formula.

$[R(x);n]$ denotes the result of the replacement of the free variable $x$ in formula $R(x)$ with the numeral (the name of the number) $n$: in modern terms: $\varphi[x/n]$.

Answer 2

In his 1931 paper, Gödel talked first (in his intro) about incompleteness relative to arithmetically sound theories (some people call this the semantic incompleteness). Notice that the background logic of Gödel's system P is higher-order (since it is a fragment of Russell's principia intended to formalize the natural numbers) so statements like "I am unprovable" isn't well-formed. x(y) is only well-formed if x is a type higher than y. In the later parts , what he proved is a Real, Syntactic Incompleteness, which doesn't care if your theory is arithmetically sound or not. This needs a crucial provability notion called representability

First, Godel needs a mechanism to 'write' such a sentence in language of first-order arithmetic. In the theorem 7 of his paper (arithmetically definable functions are closed under primitive recursion), we learned that to do this for primitive recursive functions, he needs the f(n,d,i) function (Now called the Godel Beta function). Since R has a primitive recursive property, by theorem 7 , it is arithmetical.

They key point is this: Since R is primitive recursive (Recursive in Gödel's paper), it must be representable in his formal theory. The whole point of 1-46 is to precisely tell you that these are all primitive recursive since we only applied things that preserves primtiive recursiveness.

The Gödel sentence is not some random well-formed formula that simply arises out of gimmick or paradox, but an actual sentence in the language of artihmetic. Furthermore, Matiyasevich's theorem tells us that the Gödel sentence is equivalent to a negation of diophantine.