La aritmética de Peano, según Gödel

Describimos las fórmulas del lenguaje de $\textbf{Peano}$ como sigue:

I. Las constantes: $\neg$, $\vee$, $\forall$, $0$, $S$, $($ y $)$.

II. Las variables de tipo uno (individuales, son números naturales incluyendo el $0$): $x_1, y_1, z_1, ...$

Las variables de tipo dos (clases de individuos, subconjuntos de $\mathbb{N}$): $x_2, y_2, z_2, ...$

Las variables de tipo tres (clases de clases de individuos, subconjuntos de subconjuntos de $\mathbb{N}$): $x_3, y_3, z_3, ...$

Y sigue con un tipo para cada número natural.

Una nota: las variables para las funciones de dos o más términos son superfluas como signos básicos, ya que las relaciones pueden ser definidas como clases de pares ordenados y los pares ordenados pueden ser definidos como clases de clases, por ejemplo, el par ordenado $a,b$ por $((a), (a,b))$ donde $(x,y)$ significa la clase cuyos elementos son $x$ e $y$, y $(x)$ la clase cuyo único elemento es $x$.

Por un signo de primer tipo entendemos una combinación de signos de la forma $a, S(a), S(S(a)), S(S(S(a))), ...$ donde $a$ es bien $0$ o una variable de primer tipo. En el primer caso llamamos a tal símbolo un símbolo numérico. Para $n>1$ entendemos un símbolo de tipo $n$-ésimo lo mismo que una variable de tipo $n$-ésimo. Las combinaciones de los símbolos de la forma $a(b)$, donde $b$ es un símbolo de tipo $n$ y $a$ es un símbolo de tipo $n+1$, se llaman fórmulas elementales.

Las fórmulas las definimos como la menor clase que contiene todas las fórmulas elementales y, además, con cualquier $a$ y $b$ las siguientes: $\neg(a)$, $(a)\vee(b)$, $\forall x:(a)$ (donde $x$ es cualquier variable). Llamamos a $(a)\vee(b)$ la disyunción de $a$ y $b$, a $\neg(a)$ la negación y a $\forall x:(a)$ la generalización de $a$. Una fórmula en la que no hay ninguna variable libre se llama fórmula proposicional.

Denotamos como $\text{Subst}\,a\binom{v}{b}$ (donde $a$ es una fórmula, $v$ es una variable y $b$ es un símbolo del mismo tipo que $v$) a la fórmula que se deriva a partir de $a$ reemplazando todas las ocurrencias de $v$, donde sean libres, por $b$.

Decimos que una fórmula $a$ es una elevación de tipo de otra fórmula $b$ si podemos obtener $b$ incrementando el tipo de todas las variables de $a$ por el mismo número.

Las fórmulas siguientes (I–V) son los axiomas. Los indicamos con las abreviaturas $\wedge$, $\Rightarrow$, $\iff$, $\exists$ y $=$, definidos como: $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$, y $x_1=y_1 \equiv \forall x_2:(x_2(x_1)\Rightarrow x_2(y_1))$.

I.

II. Toda fórmula derivada de insertar cualquier fórmula para $p$, $q$ y $r$ en los esquemas siguientes:

III. Cada fórmula obtenida de los dos esquemas:

haciendo las siguientes sustituciones para $a$, $v$, $b$ y $c$ (y realizando en (P8) la operación denotada por Subst): para cualquier fórmula $a$, cualquier variable $v$, para una fórmula cualquiera $b$ en la que $v$ no aparece de forma libre, y para $c$ un signo del mismo tipo que $v$, de modo que $c$ no contenga una variable que esté ligada en $a$ en un lugar donde $v$ sea libre.

IV. Cada fórmula obtenida del esquema:

insertando en el lugar de $v$ y $u$ cualquier variable de tipo $n$ y $n+1$, respectivamente, y en $a$ una fórmula sin ocurrencias libres de $u$. Este axioma es el de reducibilidad.

V. Cualquier fórmula obtenida de la siguiente mediante elevación de tipo (y la fórmula en sí misma):

Este axioma nos indica que una clase está completamente determinada por sus elementos.

Una fórmula $c$ se llama consecuencia inmediata de $a$ y $b$ si $a$ es la fórmula $(\neg(b))\vee(c)$, y una consecuencia inmediata de [únicamente] $a$ si $c$ es la fórmula $\forall v:a$, donde $v$ es cualquier variable. La clase de [teoremas] se define como la menor clase de fórmulas que contiene a los axiomas y que es cerrada bajo la operación «consecuencia inmediata».

Una fórmula de $\textbf{Peano}$ es verdadera si es cierta interpretándola como una afirmación lógica sobre los números naturales.