1

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:

enter image description here

...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?

Mauro ALLEGRANZA
  • 94,169
Zazaeil
  • 1,518
  • 1
    "Class" just means a collection; what's important here are the limitations on the contents. Letting $A_1=\mathbb{N}$ and $A_{n+1}=\mathcal{P}(A_{n})$, the variables of the $n$-th type are constrained to denote elements of $A_n$. Working with these limited sets, there's no possibility of contradiction or self-reference.... variables can only refer to variables of lower types, terminating with the natural numbers. – mjqxxxx Nov 15 '20 at 17:26
  • @mjqxxxx I still can't get it. Can you give me an example what $x_2$ and $x_1$ and $x_4$ could be with respect to natural numbers as Godel writes in his book? – Zazaeil Nov 15 '20 at 17:47

1 Answers1

2

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].

Mauro ALLEGRANZA
  • 94,169
  • Wow! That's pretty unexpected explanation that surprises me a lot. Is there a translation from outdate Godel's language to commonly used now? Or some kind of comments for people like me, who need such an explanation? – Zazaeil Nov 15 '20 at 19:28
  • And the other question - what is $x3, y3$ then? As far as I can say, it is some statements about $x2, y2$, i.e. predicates about predicates? – Zazaeil Nov 15 '20 at 19:47
  • @SerejaBogolubov - here a translation with modern symbols. – Mauro ALLEGRANZA Nov 15 '20 at 21:07