Can't understand definition of system $P$ given by Kurt Godel in his "On formally undecidable propositions..."

Question

I am reading On formally undecidable propositions of Principia Mathematica and related systems by Kurt Godel. And I am not quite sure I am getting his definitions right. See the screenshot beneath:

...and so on for every natural number as type.

What does it mean for natural number to define a type? As far as I understand $x_1$ could reference to any natural number, for example $x_1 = 12$ is correct, but it can't reference set of natural numbers, so $x_1 = \{ 12, 1 \}$ is not correct.

But what about $x_2$? What is "class of individuals"? Is it the class from the set theory (i.e. a collection of items that looks like set but can not be a set because it may lead to contradiction)? Or Kurt Godel uses term "class" to mean something different? To my understanding, $x_2 = \{ 12, 1 \}$ is correct, but $x_2 = 12$ is not.

Why do we ever need to distinct between variables?

Answer 1

It is High-Order Logic.

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.

In modern terms, Type-1 is the collections of (individual) terms: the constant $0$, and terms $f(a)$ where $f$ is the successor function.

The intended model is $\mathbb N$; thus the above terms are numerals:

$0, f(0) [i.e. 1], ff(0) [i.e.2]$, and so on.

See axiom I.1: $\lnot (fx_1=0)$. It is the first Peano axioms: number zero is not a successor.

There are no predicate constants because, being Hihg-Order Logic, we can define equality $x_1=y_1$ as follows:

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

that reads : $\forall P [P(x_1) \to P(y_1)]$.

In Gödel's symbols, $x_1,y_1$ are variables of Type-1 (ranging over individuals, i.e. numbers) while $x_2$ is a variable of Type-2 (ranging over predicates, i.e. "classes of individuals").

See axiom I.3 (Induction): $x_2(0) \cdot x_1 \Pi (x_2(x_1) \supset x_2(f(x_1)) \supset x_1 \Pi (x_2(x_1))$, that is exactly:

$P(0) \land \forall x_1 (P(x_1) \to P(f(x_1)) \to \forall x_1 (P(x_1)).$

$x_3$ is a variable of Type-3 that ranges over predicates of predicates: "classes of classes of individuals", "and so on, for every natural number as a type".

See axiom IV.1: $\exists x_{n+1}(x_n \Pi (x_{n+1}(x_n) \equiv a))$, that reads: $\exists \Psi \forall P(\Psi(P) \equiv \varphi)$.

It expresses the fact for every suitable formula ranging over Type-$n$ "objects" there is the corresponding predicate of Type-(n+1) [Comprehension axiom].