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$ Oct 29, 2015 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$ Oct 29, 2015 at 19:26

1 Answer 1



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$ Oct 16, 2016 at 9:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .