Demostrar no es lo mismo que ser verdad

No debemos creer a quienes hoy, con porte filosófico y tono deliberativo, profetizan la caída de la cultura y aceptan el ignorabimus . Para nosotros no hay ignorabimus, y en mi opinión tampoco lo hay en la ciencia natural. En oposición al necio ignorabimus nuestro lema será: «¡debemos saber — sabremos!» David Hilbert, citado en Vinnikov (1999) 1

En este capítulo nos preguntamos si podemos expresar de forma algorítmica los conceptos de demostración y verdad: si existe una forma automática de resolver teoremas y comprobar afirmaciones. Como explicamos en el Capítulo 1, este fue uno de los ejes centrales de las matemáticas de principios del siglo XX.

Las matemáticas consisten en deducir teoremas a partir de una cierta lista de axiomas. Para poder definir precisamente este concepto, recurrimos a los sistemas formales (Sección 4.1).

Sin embargo, nos interesa especialmente saber si las afirmaciones (o fórmulas) de un sistema son verdaderas. Para esto, necesitaremos definir los sistemas lógicos (Sección 4.2).

Una vez realizada la distinción entre demostrable y verdadero, nos preguntamos por la relación que estos dos conceptos tienen en un determinado sistema lógico: a partir de esto, comprenderemos en la Sección 4.3 los conceptos de solidez y completitud, y finalmente preguntaremos si podemos comprobar si una fórmula es verdadera de forma algorítmica, pudiendo decir si un sistema lógico es decidible o no (véase el Capítulo 3). A lo largo de esta sección introduciremos múltiples ejemplos de sistemas lógicos que reforzarán los conceptos ya mencionados, todos girando en torno a una operación aritmética sencilla.

A continuación, introduciremos un sistema lógico de especial importancia: la aritmética de Peano (Sección 4.4). Este sistema es capaz de demostrar una gran cantidad de teoremas de la teoría de números, por lo que nos resultará especialmente interesante saber si todas sus afirmaciones verdaderas son demostrables (este es, justamente, el Primer Teorema de Incompletitud, que demostramos en el Capítulo 5). Para ello, encontraremos una forma de traducir el problema de parada (Sección 3.6) en una fórmula de este sistema.

Finalmente, introduciremos más propiedades de los sistemas introducidos en la Sección 4.5.

4.1 #Sistemas formales

A lo largo de este trabajo hemos presentado múltiples demostraciones, pero ¿qué es exactamente una demostración? Cuando hablamos de demostrar algo, nos referimos a hacerlo de forma matemática. Al contrario que las pruebas científicas, las pruebas matemáticas son exactas y comprobables. De este modo, podemos preguntarnos si un ordenador puede realizar demostraciones de forma automática.

Para responder a todas estas preguntas, necesitaremos crear una estructura matemática que nos permita formalizar el concepto de demostración.

\mathcal{S}

Veamos un ejemplo de sistema formal que nos será extremadamente útil en este capítulo.

\textbf{SumaBinaria}

Es importante recalcar la notación usada para describir las reglas de inferencia de $\textbf{SumaBinaria}$ , en concreto, sobre el significado de coincidencia maximal. Una coincidencia maximal, en este caso, es una subcadena que verifica la expresión regular de $N$ y no puede extenderse en más direcciones. En el caso de la fórmula 100+11+1001=101, tenemos cuatro coincidencias maximales de este tipo: 100, 11, 1001 y 101, en ese orden.

Sería posible describir estas reglas mediante expresiones regulares, pero esto haría que la notación fuese menos sencilla e intuitiva.

Una vez definido un sistema formal, será posible probar (o demostrar) algunas de sus fórmulas, a las que llamaremos teoremas.

\mathcal{S}=(\mathcal{L}, \mathcal{A}, \mathcal{R})

Veamos un ejemplo de teorema en $\textbf{SumaBinaria}$ .

\textbf{SumaBinaria}

	Paso	Fórmula	Justificación
	(F1)	`1=1`	(axioma)
$\mapsto$	(F2)	`1+1=1+1`	(aplicar R1 a F1)
$\mapsto$	(F3)	`1+1=10`	(aplicar R2 a F2)
$\mapsto$	(F4)	`1+1+1=1+10`	(aplicar R1 a F3)
$\mapsto$	(F5)	`1+1+1=11`	(aplicar R3 a F4)

Observa que, aunque no esté en la definición, las demostraciones de los teoremas suelen ir acompañadas de notas que ayudan a comprobar la prueba. El repositorio intro-to-incompleteness proporciona binary_addition.py con la función es_teorema. Para probar si una fórmula es un teorema en alguno de los sistemas de este capítulo, especifica el nombre del sistema seguido de la fórmula.

A continuación, algunos ejemplos de uso de esta función:

>>> from suma_binaria import es_teorema
>>> es_teorema('SumaBinaria', '1+1+1=11')
    (F1) 1=1            (Axioma)
 -> (F2) 1+1=1+1        (R1)
 -> (F3) 1+1+1=1+1+1   (R1)
 -> (F4) 1+1+1=1+10     (R2)
 -> (F5) 1+1+1=11       (R3)
'teorema'
>>> es_teorema('SumaBinaria', '11+1=10')
'no demostrado en las primeras 109322 fórmulas generadas'
>>> es_teorema('SumaBinaria', 'mal-formada')
'fórmula mal formada'
>>> es_teorema('SistemaQueNoExiste', 'lo-que-sea')
'el sistema no existe'

La prueba de 1+1+1=11 que realiza es_teorema es diferente de la del Ejemplo 4.4. Esto es perfectamente posible: un teorema puede tener diversas demostraciones. Este hecho se evidencia de la propia Definición 4.3: una fórmula es un teorema si «existe una demostración».

4.2 #Sistemas lógicos

Como dice el propio nombre, el sistema $\textbf{SumaBinaria}$ pretende comprobar fórmulas de la suma binaria. De este modo, una palabra como 11 representa el número $3$ , y una fórmula como 1+1+1=11 representa que $1+1+1=3$ . Observa que esto nos permite reconocer si una fórmula de $\textbf{SumaBinaria}$ es verdadera: simplemente la interpretamos como si se tratase de una fórmula aritmética, y la declaramos como cierta si es una fórmula aritmética correcta. De este modo, fórmulas como 10+1=11 son verdaderas, mientras que otras como 11+1=10 no lo son.

En el apartado anterior, no mencionamos el concepto de verdad de forma intencionada: un sistema formal no tiene ninguna noción de certeza. Esto es porque las definiciones de teorema y fórmula verdadera son completamente diferentes.

Los teoremas solo dependen de la sintaxis: «¿podemos demostrar un teorema a partir de unos ciertos axiomas y unas reglas de inferencia?» La verdad, sin embargo, depende de la semántica: «¿es esta fórmula cierta cuando es interpretada dándole cierto significado a sus símbolos?»

Por definición, los sistemas formales solo dependen de la sintaxis. En esta sección, introduciremos los sistemas lógicos, que no son nada más que sistemas formales a los que le añadimos una semántica. Cuando añadimos la semántica de la aritmética que hemos comentado al sistema formal $\textbf{SumaBinaria}$ obtenemos el sistema lógico $\textbf{SumaBinariaLógico}$ .

\textbf{SumaBinariaLógico}

Formalmente, podemos definir estos sistemas como:

\mathcal{G} = (\mathcal{S}, \mathcal{I})

Una vez que incorporamos a un sistema formal una asignación de verdad, podemos decir cuándo una fórmula es verdadera. Precisamos esto en la definición siguiente:

\mathcal{G}=(\mathcal{S}, \mathcal{I})

Veamos ejemplos de fórmulas verdaderas y falsas para $\textbf{SumaBinariaLógico}$ .

\textbf{SumaBinariaLógico}

En suma_binaria.py también se proporciona una función para comprobar la veracidad de las fórmulas en sistemas lógicos, llamada es_verdadero. Un ejemplo:

>>> from suma_binaria import es_verdadero
>>> es_verdadero('SumaBinariaLógico', '1+1+1=11')
True
>>> es_verdadero('SumaBinariaLógico', '11+1=10')
False
>>> es_verdadero('SumaBinariaLógico', 'mal-formada')
False
>>> es_verdadero('SumaBinaria', '1+1+1=11')
'el sistema no existe o no es un sistema lógico'

Introduciremos más sistemas lógicos que resultarán de añadir (Sistema 4.8) y eliminar (Sistema 4.9) reglas de $\textbf{SumaBinariaLógico}$ .

\textbf{SumaBinariaLógicoRoto}

\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}

Estos sistemas son especialmente interesantes, pues en ellos podemos encontrar tanto fórmulas demostrables y no verdaderas (Ejemplo 4.10) como fórmulas verdaderas y no demostrables (Ejemplo 4.11).

\textbf{SumaBinariaLógicoRoto}

\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}

4.3 #Solidez, completitud y decidibilidad

Hemos encontrado sistemas lógicos en los que hay fórmulas verdaderas y no demostrables, y viceversa. Esto nos conduce a la definición de dos importantes propiedades de los sistemas lógicos.

Definición 4.12 — Solidez Un sistema lógico es sólido si todos sus teoremas son verdaderos. En caso contrario, decimos que es no sólido .

Definición 4.13 — Completitud Un sistema lógico es (semánticamente) completo 5 si todas las fórmulas verdaderas son teoremas. En caso contrario, decimos que es incompleto .

Veamos si los sistemas lógicos que hemos presentado hasta ahora son sólidos y completos. Un resumen de todos los resultados se puede ver en la Tabla 4.1.

Probar que $\textbf{SumaBinariaLógico}$ es sólido y completo consiste en comprobar el axioma y cada regla de inferencia frente al significado previsto de la suma binaria. Un boceto basta para ver la idea; los argumentos completos son la Proposición 4.14 y la Proposición 4.15 más abajo.

\textbf{SumaBinariaLógico}

N+N

\textbf{SumaBinariaLógico}

1=1

\textbf{SumaBinariaLógico}

\phi

Dado que los otros sistemas lógicos se «obtienen» a partir de $\textbf{SumaBinariaLógico}$ , las proposiciones siguientes son mucho más sencillas de demostrar. Como es evidente, el Ejemplo 4.10 y el Ejemplo 4.11 prueban que $\textbf{SumaBinariaLógicoRoto}$ es no sólido y que $\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}$ es incompleto, respectivamente.

Veamos a continuación tales proposiciones.

\textbf{SumaBinariaLógicoRoto}

\textbf{SumaBinariaLógico}

\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}

\textbf{SumaBinariaLógico}

Los sistemas lógicos $\textbf{SumaBinariaLógicoRoto}$ y $\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}$ los obtuvimos modificando la sintaxis de $\textbf{SumaBinariaLógico}$ . Introducimos ahora el último sistema de este tipo, que surge de modificar la semántica de $\textbf{SumaBinariaLógicoRoto}$ .

\textbf{SumaBinariaLógicoArreglado}

En este último sistema lógico podríamos haber modificado el símbolo = por >=. Sin embargo, no lo hacemos de forma intencionada, y para recordar que la sintaxis y la semántica son independientes — podemos asignar el valor de verdad que queramos.

Veamos un ejemplo sencillo e ilustrativo de fórmula verdadera y de fórmula falsa.

\textbf{SumaBinariaLógicoArreglado}

Al modificar la semántica, hemos logrado «arreglar» el sistema $\textbf{SumaBinariaLógicoRoto}$ , como bien dice su nombre. En efecto, $\textbf{SumaBinariaLógicoArreglado}$ es completo y sólido.

\textbf{SumaBinariaLógicoArreglado}

\geq

\textbf{SumaBinariaLógicoArreglado}

\phi

A modo de resumen, vemos en la tabla siguiente la completitud y solidez de los sistemas presentados (junto con otra información que veremos más adelante).

	Sólido	Completo	Decidible
$\textbf{SumaBinariaLógico}$ (reglas R1, R2, R3)	sí	sí	sí
$\textbf{SumaBinariaLógicoRoto}$ (reglas R1, R1b, R2, R3)	no	sí	sí
$\textbf{SumaBinariaLógico}\allowbreak\textbf{Restringido}$ (reglas R1, R2)	sí	no	sí
$\textbf{SumaBinariaLógicoArreglado}$ (reglas R1, R1b, R2, R3 y una semántica diferente)	sí	sí	sí
$\textbf{Peano}$	asumido	no	no

Tabla 4.1. Solidez, completitud y decidibilidad de los sistemas lógicos de este capítulo.

Adicionalmente a las propiedades de solidez y consistencia, podemos introducir una propiedad computacional: la de decidibilidad. Ya sabemos qué significa decidible para un problema de decisión: que podemos resolverlo con un programa que siempre para y tiene salida correcta. Para un sistema lógico $\mathcal{G}$ podemos definir un problema de decisión, $\textsc{EsVerdadero}_\mathcal{G}$ .

_\mathcal{G}

Para cada sistema lógico $\mathcal{G}$ obtenemos un problema de decisión distinto. Una vez definido este problema, es natural definir la decidibilidad de un sistema lógico mediante la decidibilidad del problema.

\mathcal{G}

De este modo, un sistema lógico es decidible si existe un programa que decide si una fórmula es verdadera o no. Es importante notar que algunos autores definen como sistema decidible aquel en el que el problema $\textsc{EsTeorema}_\mathcal{S}$ (que definimos a continuación) es decidible. Como hemos visto, la verdad y la demostración son conceptos diferentes, y nosotros nos referiremos siempre a la verdad al preguntarnos por si un sistema lógico es decidible.

_\mathcal{S}

Veamos si los sistemas lógicos que hemos introducido en este capítulo son decidibles. En el caso de $\textbf{SumaBinariaLógico}$ , es sencillo crear un programa que sea capaz de comprobar si las fórmulas que se insertan están bien formadas, y que comprueba si la operación aritmética es correcta. De hecho, este programa está implementado: es la función es_verdadero de suma_binaria.py:

>>> from suma_binaria import es_verdadero
>>> es_verdadero('SumaBinariaLógico', '1+1+1=11')
True
>>> es_verdadero('SumaBinariaLógico', '11+1=10')
False

En el caso del resto de sistemas lógicos, crear programas que los decidan resulta igual de sencillo. Las implementaciones a estos programas se encuentran igualmente en es_verdadero. Vemos a continuación más ejemplos de la ejecución de esta función en el resto de sistemas lógicos.

>>> from suma_binaria import es_verdadero
>>> es_verdadero('SumaBinariaLógico', '11=1+1')
False
>>> es_verdadero('SumaBinariaLógicoRoto', '11=1+1')
False
>>> es_verdadero('SumaBinariaLógicoRestringido', '11=1+1')
False
>>> es_verdadero('SumaBinariaLógicoArreglado', '11=1+1')
True

4.4 #La aritmética de Peano

Los sistemas lógicos que hemos explorado son de poca utilidad. Lo que queremos es trabajar con sistemas lógicos que permitan probar resultados interesantes en matemáticas. Los matemáticos, lógicos y filósofos han estudiado multitud de sistemas lógicos desde finales del siglo XIX, pero dos destacan por su importancia: los axiomas de Zermelo–Fraenkel, de teoría de conjuntos, y la aritmética de Peano, de teoría de números. En este apartado nos centraremos en el último, pues la aritmética de Peano contiene fórmulas sobre enteros, adición, multiplicación, etc.

Llamaremos $\textbf{Peano}$ al sistema lógico de la aritmética de Peano. Puedes encontrar la descripción completa de este sistema en Aritmética de Peano. En la Figura 4.22 puedes encontrar algunos detalles de tal descripción.

\textbf{Peano}

En este sistema podemos producir fórmulas sobre aritmética muy interesantes. Vemos algunas de ellas a continuación.

\textbf{Peano}

Para poder trabajar con $\textbf{Peano}$ en programas en Python, deberemos encontrar una forma de codificar los diversos símbolos, que especificamos en la Tabla 4.2.

Símbolo	Codificación	Descripción
$\neg(p)$	`NO (p)`	Negación
$(p) \vee (q)$	`(p) Ó (q)`	Disyunción
$\forall x : p$	`PARA TODO (x) : (p)`	Cuantificador universal
$S(a)$	`S(a)`	Sucesor
$\exists x : p$	`EXISTE (x) : (p)`	Cuantificador existencial
$(p) \Rightarrow (q)$	`(p) => (q)`	Implicación
$(p) \iff (q)$	`(p) <=> (q)`	Coimplicación
$(p) = (q)$	`(p) = (q)`	Igualdad

Tabla 4.2. Una forma de traducir los símbolos de la aritmética de Peano a strings.

Por ejemplo, consideremos la afirmación «no existen enteros $x$ e $y$ de modo que $2x=y$ e $y=3$ », que puede representarse en $\textbf{Peano}$ como $\neg\exists x, y : S(S(0)) \cdot x = y \wedge y = S(S(S(0)))$ y que admite la siguiente codificación en string:

NO EXISTE x,y : S(S(0))*x = y Y y = S(S(S(0)))

Las fórmulas de $\textbf{Peano}$ , por ser de un sistema lógico, pueden ser verdaderas o falsas. En el Ejemplo 4.23, las primeras seis fórmulas (de (PF1) a (PF6)) son verdaderas,⁸⁹ mientras que la última (la fórmula (PF7)) es falsa.

Para poder probar si una fórmula de $\textbf{Peano}$ es verdadera, necesitamos que sea cerrada: esto ocurre si todas sus variables son cuantificadas por un «para todo» ( $\forall$ ) o un «existe» ( $\exists$ ).¹⁰ Un ejemplo de esto es $\forall x,y : x=y \wedge x+S(0)=y+S(0)$ , que es una fórmula cerrada pues $x$ e $y$ son cuantificadas, mientras que $x=y \wedge x+S(0)=y+S(0)$ no es una fórmula cerrada. Esta distinción es importante porque, si una fórmula no es cerrada, no podemos saber si es verdadera. Solo consideraremos fórmulas cerradas en $\textbf{Peano}$ de aquí en adelante.

Una vez que aceptamos que la aritmética de Peano puede expresar afirmaciones matemáticas como las del Ejemplo 4.23, podemos continuar para expresar las salidas de un programa en $\textbf{Peano}$ . La siguiente proposición muestra cómo hacerlo para un conjunto concreto de fórmulas sobre los programas que necesitaremos más adelante.¹¹

P

q_R\;:\;X\:X\:\boxed{X}\:X\:a \;\;\;\; \longrightarrow \;\;\;\; \texttt{q\_R : X X \^{}X X a}

De la prueba anterior, es evidente que la construcción de $\phi_H$ a partir de $H$ se realiza de una forma completamente algorítmica, que podría en principio ser implementada por un programa en Python. Sea tal programa parada_a_peano.py. En intro-to-incompleteness no se proporciona un programa que implemente esto, ya que hacerlo es una tarea compleja.¹³ Sin embargo, en el resto de este capítulo, importaremos la función main parada_a_peano cuando sea necesario.

Definiremos a continuación dos problemas de decisión importantes: EsTeoremaPeano y EsVerdaderoPeano.¹⁴

\phi

\phi

Dada una afirmación $\phi$ en $\textbf{Peano}$ , los problemas anteriores preguntan si $\phi$ es demostrable y/o verdadera. Resulta que ambos problemas son no decidibles. La no decidibilidad de EsVerdaderoPeano nos indica, mediante la Definición 4.20, que $\textbf{Peano}$ no es decidible (como ya adelantamos en la Tabla 4.1).¹¹

\textbf{Peano}

\textsc{ParadaEnVacío}

Programa 4.1 — parada_en_vacio_a_es_verdadero_peano.py from es_verdadero_peano import es_verdadero_peano # oráculo from parada_a_peano import parada_a_peano # NO es un oráculo def parada_en_vacio_a_es_verdadero_peano (programa): para_en_peano = parada_a_peano(programa) return es_verdadero_peano(para_en_peano)

Proposición 4.28 EsTeoremaPeano es no decidible.

\textsc{ParadaEnVacío} \leq_T \textsc{EsVerdaderoPeano}

El caso de EsTeoremaPeano es menos grave, pues el problema es, de hecho, semidecidible (ver Definición 3.20). Esto quiere decir que podemos escribir un programa que compruebe si una fórmula es un teorema (en caso de que la fórmula no sea un teorema, el programa no tiene por qué parar).¹¹

Proposición 4.29 EsTeoremaPeano es semidecidible.

\textbf{Peano}

Programa 4.2 — es_teorema_peano.py import utilidades from es_prueba_peano import es_prueba_peano # NO es un oráculo def es_teorema_peano (fórmula): demostración ='' while True : if es_prueba_peano(demostración, fórmula) =='sí' : return'sí' demostración = utilidades.siguiente_string(demostración)

El hecho de que EsTeoremaPeano sea semidecidible es extremadamente importante, y se debe a una propiedad sintáctica de $\textbf{Peano}$ : es recursivamente axiomatizable.

\mathcal{S}

Decir que un sistema lógico $\mathcal{G}$ es recursivamente axiomatizable no es más que decir que el problema $\textsc{EsTeorema}_\mathcal{G}$ es semidecidible. Esta propiedad es fundamental para la prueba que realizaremos del Primer Teorema de Incompletitud (Teorema 5.2), pues si $\textbf{Peano}$ no fuese recursivamente axiomatizable, no podríamos usar la función es_teorema_peano.

El problema EsTeorema guarda una fuerte relación con el Entscheidungsproblem (ver Capítulo 1). Este problema pretende encontrar un algoritmo general que, dada una afirmación matemática, determine si es un teorema. Por la Proposición 4.28, EsTeoremaPeano es no decidible, lo cual prueba el Entscheidungsproblem en el caso particular de la aritmética de Peano. El argumento que hemos realizado es similar al que hizo Turing en ¹⁷.

Finalmente, dado que $\textbf{Peano}$ es un sistema lógico, nos podemos preguntar por su solidez y completitud. La pregunta sobre si $\textbf{Peano}$ es completo es el objeto central de este trabajo, y se tratará en el Capítulo 5.

Preguntarnos por la solidez de $\textbf{Peano}$ es una pregunta compleja. En este trabajo, asumiremos su solidez, dado que es razonable que los teoremas de $\textbf{Peano}$ sean verdaderos.¹⁸

4.5 #Completitud sintáctica y consistencia

Los libros de lógica son extremadamente inconsistentes¹⁹ al definir propiedades de sistemas lógicos (incluso al definir qué es un sistema formal y un sistema lógico). Por ahora, hemos definido las propiedades de solidez, completitud (semántica) y decidibilidad. Existe otra definición de completitud que depende únicamente de la sintaxis, y que por tanto es aplicable para sistemas formales.²⁰

\mathcal{S}

Para esta definición, el lenguaje formal debe incluir una noción bien definida de negación ( $\neg$ ). Es el caso de teorías de primer orden como la aritmética de Peano o la teoría de conjuntos de Zermelo–Fraenkel, aunque la negación también está disponible en otros lenguajes lógicos.

Para esta clase de sistemas también es posible definir una nueva propiedad: la consistencia. Nuevamente, podemos definir dos tipos de consistencia, una sintáctica y una semántica.

\mathcal{S}

\mathcal{G}

En otras palabras, un sistema es consistente si no da lugar a demostraciones o a verdades contradictorias. En un sistema sólido y completo, una fórmula es consistente sintácticamente si y solo si lo es semánticamente.

Es importante hacer una apreciación respecto a las definiciones de completitud y consistencia sintácticas: a pesar de que las definimos para sistemas formales, es sencillo extender esta definición a sistemas lógicos, teniendo en cuenta su sintaxis.

De este modo, decimos que un sistema lógico $\mathcal{G}$ es sintácticamente completo si, dada una fórmula $\phi$ de $\mathcal{G}$ , $\phi$ o $\neg\phi$ son teoremas. Análogamente, $\mathcal{G}$ es sintácticamente consistente si no es posible que tanto $\phi$ como $\neg\phi$ sean teoremas.

Las definiciones que hemos hecho hasta este punto (sin incluir la de decidibilidad) se encuentran resumidas en la Figura 4.34.

\mathcal{G}

Vinnikov, V. (1999). We shall know: Hilbert's apology. Mathematical Intelligencer, 21(1):42–46.
↩
Siempre que hablamos de fórmulas nos referimos a fórmulas bien formadas.
↩
Aquí el símbolo de suma + es un literal, no el operador $+$ .
↩
Cuando una fórmula no está bien definida o no tiene una interpretación definida, podemos asumir que es falsa.
↩
Más adelante introducimos la noción de completitud sintáctica (Definición 4.31). Siempre que llamemos a un sistema completo, sin especificar, nos referiremos a su completitud semántica.
↩
Se pueden traducir sencillamente a aritmética de Peano. Por ejemplo, (PF2) es $\forall x : x^2+1>0$ , y (PF6) es $\forall n>2 : \neg\exists x,y,z>0 : x^n+y^n=z^n$ . Aunque las operaciones de comparación y exponenciación no estén inicialmente definidas en $\textbf{Peano}$ , podemos definirlas mediante fórmulas del sistema.
↩
$f^3$ significa iterar $f$ tres veces: $f^3(x)=f(f(f(x)))$ .
↩
El último teorema de Fermat tiene especial relevancia histórica: fue formulado en 1637 y no fue resuelto hasta el año 1995 por Andrew Wiles.
↩
Wiles, A. (1995). Modular elliptic curves and Fermat's Last Theorem. Annals of Mathematics, 141(3):443–551.
↩
Recuerda que en la Definición 4.6 dijimos que la asignación de verdad puede estar definida para un subconjunto de las fórmulas.
↩
MacCormick, J. (2018). What Can Be Computed? Princeton University Press.
↩ ↩² ↩³
Probamos la equivalencia en el Teorema 2.23.
↩
Henderson, J. (2013). Gödel's First Incompleteness Theorem in Python. https://github.com/johnyf/godel_py
↩
Observa que $\textsc{EsTeoremaPeano} = \textsc{EsTeorema}_{\textbf{Peano}}$ y $\textsc{EsVerdaderoPeano} = \textsc{EsVerdadero}_{\textbf{Peano}}$ (véanse el Problema 4.21 y el Problema 4.19).
↩
Usamos $H$ del inglés halting.
↩
Si $\mathcal{S}$ es infinito, el programa correrá infinitamente.
↩
Turing, A.M. (1937). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42(1):230–265.
↩
Puedes ver tales axiomas en Aritmética de Peano.
↩
Nótese la ironía.
↩
Kleene, S.C. (1971). Introduction to Metamathematics. North-Holland.
↩
Es decir, que en el sistema formal esté bien definida la noción de negación ( $\neg$ ).
↩
Es posible que tanto $\phi$ como $\neg\phi$ sean teoremas.
↩

4.1 #Sistemas formales

4.2 #Sistemas lógicos

4.3 #Solidez, completitud y decidibilidad

4.4 #La aritmética de Peano

4.5 #Completitud sintáctica y consistencia

Notas al pie