I am trying to understand Gödel's first incompleteness theorem from his original 1931 paper.

Here is a translation i am using for my studies :


I feel like i now have a decent intuitive understanding of it all.

Now I'm trying to understand all the technical details of it.

I don't fully understand these so called "elementary-formulae", and how it makes sense of my intuitive understanding of what they are :

For example, i suppose "$y = x+1$" is an elementary formula, how does that fit that "elementary-formulae" a(b) with 'a' a type-n+1 variable and 'b' a type-n variable.

I figure "$y = x+1$" would be "captured" by the type-3 variable :

{ (0,1), (1,2), ..., (n,n+1) }

= { {{0},{0,1}}, {{1},{1,2}}, ..., {{n},{n,n+1}} }

how would i write it as :

"'type-n+1 variable' ( 'type-n variable' ) " ?

Or can someone give me some examples of elementary formulae in the Gödel context ?

Thank you.


Unfortunately, the formal language of Gödel's paper is today quite unused :

By a sign of type $1$ we understand a combination of signs that has [anyone of] the forms

$$a, fa, ffa, fffa, \ldots,$$

and so on, where $a$ is either $0$ or a variable of type $1$. In the first case, we call such a sign a numeral. [...] A combination of signs that has the form $a(b)$, where $b$ is a sign of type $n$ and a a sign of type $n + 1$, will be called an elementary formula.

Thus [see note 21 of standard translation] "$=$" is not a primitive sign, but is defined with quantification on second-order (unary) predicate variables. The simple formula :


in Gödel's system is :

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

and thus it is not an elementary one.

As you can see, Gödel introduces only (unary) predicates :

Remark: Variables for functions of two or more argument places (relations) need not be included among the primitive signs since we can define relations to be classes of ordered pairs, and ordered pairs to be classes of classes; for example, the ordered pair $a, b$ can be defined to be $((a), (a, b))$, where $(x, y)$ denotes the class whose sole elements are $x$ and $y$, and $(x)$ the class whose sole element is $x$.

Thus, the only elementary formulae are like : $x_2(x_1)$ or $x_2(f0)$.

If we restrict ourselves to the more usual first-order language of arithmetic, the only elementary formulae are expressions like :


where $t,s$ are terms, i.e. (individual) variables, the constant $0$ or "complex" terms like the numerals: $ff \ldots f0$.

To be formal, instead of e.g. $x=f0$, we have to write :


Thus, taking into account that :

  1. $E(x) = R(11)*x*R(13)$,

i.e. $E(x)$ corresponds to the operation of "enclosing within parentheses", we have to modify the definition :

  1. $Elf(x) = (\exists y, z, n)[y, z, n \le x \land Typ_n(y) \land Typ_{n+1}(z) \land x = z*E(y)]$,

i.e. the relation encoding "$x$ is an ELEMENTARY FORMULA", in order to take into account binary relations.

In Peter Smith's book, Ch.20 Arithmetization in more details, page 144-on, you can find the def for the first-order language with "$=$" as primitive :

R13. The property $Atom(n)$ which holds when $n$ is the g.n. of an atomic wff is primitive recursive.

$Atom(n) \overset{def}{=} (∃x ≤ n)(∃y ≤ n)[Term(x) ∧ Term(y) ∧ n = (x* \ulcorner = \urcorner *y)]$.

Thus, in our "simplified" example: $=(x,f0)$, we have that $=$ is a sign of Type $2$ (it is a predicate) while $x$ (a variable) and $f0$ (a numeral) are terms, i.e. signs of Type 1.

  • $\begingroup$ thank you for your answer. Let me rephrase : if i'm correct, an elementary formulae is a(b) with 'a' being the '=' sign, hence (i guess) the set of sets { {1,1}, ... , {n,n}, ... } a type 3 variable and 'b' being ... { {x}, {x, f0} } a type 2 varible, or {x, f0}, a type 2 variable ? $\endgroup$ – joseph M'Bimbi-Bene Oct 29 '15 at 21:02
  • $\begingroup$ @MauroALLEGRANZA: Gödel's paper deals with the system of Russell and Whitehead's *Principia Mathematica", not some system of his own devising as your answer suggests. $\endgroup$ – Rob Arthan Nov 1 '15 at 21:33
  • $\begingroup$ @RobArthan - not exactly; see van Heijennort, page 595 (first para of G's paper) : "If to the Peano axioms we add the logic of Principia mathematica (with the natural numbers as the individuals) together with the axiom of choice (for all types), we obtain a formal system $S$, for which the following theorems hold ...". For the details of arithmetization (at the level required by the OP) we have to stay closer to G's system. $\endgroup$ – Mauro ALLEGRANZA Nov 2 '15 at 8:18
  • $\begingroup$ Thank you for your reply and please excuse me for answering late. The thing is that i don't understand the PM notation and logic. I have the 1962 translation but it doesn't explain much. It is hard to get a hand on a copy of principia mathematica and even then, it's not very accessible. I still managed to find it there : quod.lib.umich.edu/cgi/t/text/… I don't know exactly how to make sense of x2Π(x2(x1)→x2(fy1)) . you defined x2 as an unary predicate sign $\endgroup$ – joseph M'Bimbi-Bene Nov 6 '15 at 10:55
  • $\begingroup$ you said in one of my other post that you didn't understand my "set of set thing", but it's Gödel himself who talks about it : Variable of type one (for individuals, i.e. natural numbers including 0): Variables of type two (for classes of individuals , i.e. subsets of IN ): Variables of type three (for classes of classes of individuals , i.e. sets of subsets of N ): And so on for every natural number as type. We call combinations of signs of the form a(b), where b is a sign of type n and a a sign of type n + 1, elementary formulae. $\endgroup$ – joseph M'Bimbi-Bene Nov 6 '15 at 10:59

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.