¿Hay tipos de aritmética que son decidibles a pesar del teorema de Gödel?

Sí, hay aritmética decidible. Pero la prueba original de Gödel de 1931 estaba en el marco de los Principia Mathematica de Russell, elegido porque era el marco lógico más desarrollado para reproducir todas las matemáticas en ese momento. Posteriormente simplificó la prueba y demostró que la Aritmética de Peano era suficiente.

En la línea de su primera sugerencia, está la aritmética de Presburger , introducida en 1929, aproximadamente un año antes de que Gödel obtuviera su resultado. Tiene suma, igualdad e incluso inducción, pero no multiplicación. La ausencia de multiplicación excluye la definición de numeración de Gödel y, por lo tanto, la construcción de oraciones de Gödel. Esto no es una prueba de integridad, pero explica por qué se mantiene retroactivamente, Presburger mismo produjo un algoritmo de decisión explícito. Un algoritmo puede ser, pero no es demasiado fácil, Fischer y Rabin demostraron en 1974 que la complejidad computacional del problema de decisión es doblemente exponencial. Un hecho interesante sobre la diferencia entre las dos aritméticas: Glivický y Kalaprodujo recientemente un modelo de aritmética de Presburger donde falla el último teorema de Fermat, y hay infinitos contraejemplos. Se cree que esto no puede suceder para la aritmética de Peano, aunque esto no se deduce técnicamente de la prueba de Wiles, consulte ¿Hay contraejemplos no estándar para el último teorema de Fermat?

No es tan fácil implementar las otras dos sugerencias porque la finitud es propiedad de un modelo, no de una teoría formal. Los intentos de escribir la finitud en axiomas (de primer orden), a la Dedekind, por ejemplo, producen algo que no es lo que intuitivamente significa (hay infinitos modelos de teorías que "afirman" que los axiomas son finitos). Sin embargo, si nos conformamos con un modelo con dominio finito en lugar de una teoría de primer orden, eso, por supuesto, será decidible, porque se pueden verificar todas las posibilidades mediante una búsqueda exhaustiva.

Existe un tipo de aritmética con modelos finitos, que conserva todos los recursos de la aritmética de Peano, pero reemplaza la lógica clásica por la lógica paraconsistente LP. Estas son las aritméticas inconsistentes de Priest . Nótese una sutileza en la noción de completitud para modelos inconsistentes: mientras existe un procedimiento de decisión que asigna verdadero/falso a cada enunciado, habrá algunos a los que les asigne ambos , llamados contradicciones verdaderas o dialetheias.. La razón por la que podemos tener un modelo finito es que podemos tener "enteros inconsistentes" para los cuales n=n+1, esto lleva a una verdadera contradicción pero no trivializa la teoría, paraconsistente como es. De hecho, para todos los números más pequeños que el número N menos inconsistente, el modelo es idéntico a la aritmética habitual de Peano, y Priest argumenta que no podemos saber qué es "verdadero" de los objetos en nuestro mundo si N es exorbitantemente grande, vea su ¿Cuál podría ser el número menos inconsistente?

Esto reivindica la opinión paradójica de Wittgenstein de que la incoherencia no es un problema para las matemáticas de cálculo (o cualquier juego de lenguaje), y su anticipación de las lógicas paraconsistentes:

" Algo me dice que una contradicción en los axiomas de un sistema realmente no puede hacer ningún daño hasta que se revela. Pensamos en una contradicción oculta como una enfermedad oculta que hace daño aunque (y quizás precisamente porque) no lo hace. t se muestra de una manera obvia, pero dos reglas en un juego que en un caso particular se contradicen están perfectamente en orden hasta que se presenta el caso, y es solo entonces que se vuelve necesario tomar una decisión entre ellas por una regla adicional … Pues bien, no saques conclusiones de una contradicción, haz de eso una regla. ”

Un ejemplo importante es la aritmética habitual de los números reales : un famoso teorema de Tarski es que la teoría de los campos cerrados reales es decidible.

Desde cierto punto de vista, la dificultad de la aritmética de números enteros se debe precisamente a que no hay suficientes: la complejidad de la teoría de números proviene de que hay tantas ecuaciones que no tienen solución. Si te permites sacar raíces de polinomios (y poder sacar los números reales de los complejos), la teoría se simplifica mucho.

Si la respuesta de Conifold pierde el punto en absoluto, dado lo expansiva que es, entonces debe querer decir "¿Por qué Goedel eligió la aritmética?" Y la respuesta tiene que ser que el procedimiento de construcción sería demasiado extraño en cualquier otra forma.

Lo que es importante, filosóficamente, es que una lógica más fuerte no siempre puede hacer que las cosas sean más decidibles. La aritmética no viene al caso. Pero está tan arraigado en nosotros que no tiene sentido evitarlo.

Sabemos que ZF no está completo porque podemos desarrollar la aritmética a partir de la teoría de conjuntos, dado el enfoque estándar de definir los números enteros como una torre de segmentos iniciales de "omega". Por lo tanto, no tenemos que comenzar con la aritmética siempre que lo logremos en el camino. En el caso de la teoría de conjuntos, no es nuestra principal preocupación.

Me parece que sabemos que el verdadero problema depende de alguna manera de la fuerza de la inducción que respalda la recursividad. La inducción reducida al conjunto infinito de axiomas que siguen siendo de primer orden no le proporciona una prueba. Obtiene la aritmética de Presburger, que no es lo suficientemente fuerte como para fallar, a menos que salga del sistema y calcule previamente varios hechos de multiplicación que normalmente se deducen a través de la inducción completa sobre la suma.

Ni siquiera necesita necesariamente una inducción completa de segundo orden, que es parte de la definición original de Peano. Salimos con una pasada de inducciones para establecer el comportamiento de la suma y definir la multiplicación, pero luego solo necesitamos la versión de primer orden para la segunda pasada de inducciones.

Evidentemente, dos pases de inducción matarán su capacidad para definir la verdad en su sistema. Si desea un sistema fuerte y consistente, uno no es suficiente y dos son demasiados.

Podemos imaginar que una forma no aritmética de ver esto todavía implicaría algún concepto de conteo para basar el equivalente de la inducción, pero los conceptos alternativos de conteo parecen una pérdida de tiempo.