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 :


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.

  • $\begingroup$ For Peter Smith's book, see Ch.5 Capturing numerical properties, page 36-on, for the general concept, and Ch.16 Capturing p.r. functions, page 119-on. $\endgroup$ – Mauro ALLEGRANZA Oct 29 '15 at 19:23
  • $\begingroup$ I totally understand the general concept, at least for "regular" theory of arithmetic. I would like a more detialed proof of it $\endgroup$ – joseph M'Bimbi-Bene Oct 29 '15 at 19:26


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 :

$R(x_1,y_1)$ iff $x_1=y_1+1$

we have to use the formula :

$$x_2 \Pi (x_2(x_1) \to x_2(fy_1)).$$

As you can see, it is a generalization; thus, Def.22 applies, and not Def.20.

  • $\begingroup$ Hello, out of frustration, i let gödel go a year ago. Now i'm back. I have an intuition about the definition of the equality, but i still don't know how to actually use it. How would you prove 0=0 or 1=1 or refute 1=0 with that notation ?. Thank you $\endgroup$ – joseph M'Bimbi-Bene Oct 16 '16 at 9:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.