understanding gödel's 1931 paper - elementary formulae

Question

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 :

http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

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.

Answer 1

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 :

$$x_1=y_1+1$$

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 :

$t=s$

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 :

$=(x,f0)$.

Thus, taking into account that :

10. $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 :

20. $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.