I am trying to fully understand gödel's proof of the first incompleteness theorem from it's original 1931 paper.
Here is the document I am using :
http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf
My question is : can someone give me or help me figure out a satisfying proof of that theorem V ?
"For every primitive recursive relation $R(x_1 , . . . , x_n )$ there is a relation sign $r$ (with the free variables $u_1 , . . . , u_n$ ), such that for each n-tuple $(x_1 , . . . , x_n )$ the following holds:
$R(x_1 , . . . , x_n ) ⇒ provable(subst(r, u_1 . . . u_n , number(x_1 ) . . . number(x_n )))$ $¬R(x_1 , . . . , x_n ) ⇒ provable(not(subst(r, u_1 . . . u_n , number(x_1 ) . . . number(x_n ))))$ "
the question has already been answered here : Proof of Proposition/Theorem V in Gödel's 1931 paper?
But i don't really understand the answer : in the case of the "primitive recursion", I don't understand what is that "finite sequence σ" all about and even in the case of the simpler functions, like the "successor" one :
"For the successor function $R(x)=x+1$, let $r(x,y)$ be $y=x+1$"
How, in the system introduced by gödel, would even "prove" that ?
In the system he introduced, there is no symbol for functions or how to construct arithmetical formulae. As far as i understand it, we would just have to define its so-called "extension" rather than its expression as a "formula".
Taking once again the example introduced earlier, from what i understand, the relation
$r(x,y) <=> y=x+1$ would be defined as a type 3 variables :
{ (0,1), (1,2), ..., (n,n+1) }
= { {{0},{0,1}}, {{1},{1,2}}, ..., {{n},{n,n+1}} }
But it doesn't have to be "proven", we would just have to "introduce" the associated type-n variable.
And even in a "regular" system of arithmetic, with symbols for the addition, multiplication, functions, etc. how one would prove it.
I could not find a proof in the Peter Smith book : "An Introduction to Gödel’s Theorems" in the chapter 12-13 as indicated in the answer (i overlooked chapters 4 to 13 and couldn't find it anywhere). Only the statement of that theorem.
Thank you.
Hint
You can find the result in every math log textbook; the proof is outlined into Carl Mummert's answer you have referenced.
But the details of the proof are dependent on the details of the language: "modern" textbooks usually refers to first-order language for arithmetic, where, for example $=$ is primitive (a basic sign) while in G's original paper it is defined.
Thus, if you want to work with G's original language, you have to stay closer to it; thias means that $=(x,0)$ is not an elementary formula of the system.
Regarding the "simplest" case :
we have to use the formula :
As you can see, it is a generalization; thus, Def.22 applies, and not Def.20.