Peano arithmetic, as Gödel wrote it

We describe the formulas of the language of $\textbf{Peano}$ as follows:

I. Constants: $\neg$, $\vee$, $\forall$, $0$, $S$, $($ and $)$.

II. Variables:

• Type-one variables (individuals, i.e. natural numbers including $0$): $x_1, y_1, z_1, ...$
• Type-two variables (classes of individuals, i.e. subsets of $\mathbb{N}$): $x_2, y_2, z_2, ...$
• Type-three variables (classes of classes of individuals): $x_3, y_3, z_3, ...$
• And so on for each natural number type.

Note: variables for functions of two or more terms are superfluous as basic signs, since relations can be defined as classes of ordered pairs and ordered pairs can be defined as classes of classes.

A sign of first type is a combination of signs of the form $a, S(a), S(S(a)), S(S(S(a))), ...$ where $a$ is either $0$ or a type-one variable. In the first case we call it a numeral. For $n>1$, a sign of type $n$ is a type-$n$ variable. A combination of the form $a(b)$, where $b$ is a type-$n$ sign and $a$ is a type-$(n+1)$ sign, is called an elementary formula.

The formulas are defined as the smallest class containing all elementary formulas and, moreover, with any $a$ and $b$ the following: $\neg(a)$, $(a)\vee(b)$, $\forall x:(a)$ (where $x$ is any variable). We call $(a)\vee(b)$ the disjunction of $a$ and $b$, $\neg(a)$ the negation, and $\forall x:(a)$ the generalization of $a$. A formula with no free variables is called a propositional formula.

We write $\text{Subst}\,a\binom{v}{b}$ (where $a$ is a formula, $v$ is a variable, and $b$ is a sign of the same type as $v$) for the formula obtained from $a$ by replacing all free occurrences of $v$ by $b$.

A formula $a$ is a type elevation of $b$ if $b$ can be obtained by increasing the type of all variables of $a$ by the same number.

The following formulas (I–V) are the axioms. We use the abbreviations $\wedge$, $\Rightarrow$, $\iff$, $\exists$ and $=$, defined as: $p\wedge q \equiv \neg(\neg p\vee\neg q)$, $p\Rightarrow q \equiv \neg p\vee q$, $p\iff q \equiv (\neg p\vee q)\wedge(\neg q\vee p)$, $\exists x:p \equiv \neg\forall x:\neg p$, and $x_1=y_1 \equiv \forall x_2:(x_2(x_1)\Rightarrow x_2(y_1))$.

I.

II. Every formula derived by inserting any formulas for $p$, $q$ and $r$ in:

III. Each formula obtained from:

by substituting any formula for $a$, any variable for $v$, any formula not containing $v$ free for $b$, and a sign of the same type as $v$ for $c$ (not containing a variable that is bound in $a$ where $v$ is free).

IV. Each formula obtained from:

inserting type-$n$ and type-$(n+1)$ variables for $v$ and $u$ respectively, and any formula with no free occurrences of $u$ for $a$. This is the axiom of reducibility.

V. Any formula obtained from the following by type elevation (and the formula itself):

This axiom states that a class is completely determined by its elements.

A formula $c$ is an immediate consequence of $a$ and $b$ if $a$ is $(\neg(b))\vee(c)$, and an immediate consequence of $a$ alone if $c$ is $\forall v:a$ for some variable $v$. The class of theorems is defined as the smallest class of formulas containing the axioms and closed under the operation "immediate consequence".

A formula of $\textbf{Peano}$ is true if it is true when interpreted as a logical statement about the natural numbers.