El teorema de incompletitud de Gödel y lógicas/sistemas fundacionales no estándar

Soy aficionado en el campo de la lógica matemática, así que lo siento por las partes confusas de esta pregunta.

Es bien sabido que el teorema de incompletitud de Gödel muestra que existen grandes límites para lo que puede hacer la lógica de primer orden. ¿Es posible basar nuestro razonamiento formal en algún otro sistema (diferente tipo de lógica, teoría de tipos (?), algo basado en la teoría de categorías) de tal manera que no se aplique el teorema de incompletitud de Gödel?

¿Alguien ha intentado inventar un sistema completamente nuevo como base de las matemáticas para evitar esto? ¿Quizás uno no basado en fórmulas y pruebas, sino en algo completamente diferente?

La lógica infinita está libre de los teoremas de Gödel. En realidad, eso se debe a que la lógica infinitaria no es recursiva.
Necesitará restricciones más estrictas que "razonar en algún otro sistema de tal manera que el teorema de incompletitud de Gödel no se aplique" para que la pregunta sea interesante. Se aplica explícitamente a las teorías de primer orden, que incluyen la aritmética de Peano, recursivamente axiomatizables y consistentes, cualquiera de las anteriores puede ser, y ha sido descartada, pero no sin un costo. La aritmética paraconsistente completa existe, por ejemplo, la geometría elemental de Tarski está completa, etc.
Si también está interesado en las pruebas de consistencia, le gustaría saber que es posible probar la consistencia de la aritmética utilizando la lógica de relevancia. Para ser más precisos, si crea aritmética relevante agregando los axiomas de Peano a la lógica de relevancia, esta aritmética es demostrablemente absolutamente consistente usando métodos finitos. La lógica de relevancia es más débil que la clásica, por lo que la aritmética relevante no contiene todos los teoremas de la aritmética clásica. Véase Meyer y Friedman, 1992, “Whither Relevant Arithmetic?”, The Journal of Symbolic Logic, 57: 824–831.
Claramente no entendiste los teoremas de incompletitud de Gödel, casi con seguridad porque el relato popular que leíste es incorrecto o engañoso. El resultado original de Gödel fue para una teoría clásica de la aritmética de primer orden, pero los teoremas de incompletitud generalizados son válidos para cualquier sistema fundamental razonable para las matemáticas, incluso aquellos que aún no han sido concebidos. Como se indica en la publicación vinculada, es falso que se aplique solo a FOL, o solo a sistemas deductivos que involucran fórmulas convencionales.
En particular, no importa qué tipo de sistema fundacional exótico tenga, si tiene un programa verificador de prueba y puede razonar sobre los programas, entonces es inconsistente (prueba afirmaciones contradictorias sobre los programas) o incompleto (no prueba que P se detiene en X, para algún programa P que realmente se detiene en la entrada X). Las condiciones son satisfechas por cualquier sistema fundacional razonable S, porque para que S sea utilizable en primer lugar, debe tener un programa verificador de prueba, y si S ni siquiera puede razonar sobre la ejecución finita del programa, entonces es demasiado débil para ser fundacional.
La teoría de autoverificación de Dan Willard no puede razonar sobre programas. Por lo tanto, es inadecuado para una base de matemáticas. Si es adecuado para el razonamiento diario o no es una pregunta separada (y potencialmente interesante).

Respuestas (2)

Hay un gran número de formas de eludir la prueba de Gödel. La pregunta es si esos sistemas tienen suficiente valor práctico para las matemáticas para ser utilizados para cualquier propósito que no sea el de eludir su demostración.

Mi solución favorita personal es el trabajo de Dan Willard: Sistemas de axiomas de autoverificación, el teorema de incompletitud y los principios de reflexión relacionados. . En él, creó un sistema que podía probar todas sus propias afirmaciones verdaderas y contenía todas las verdades de la aritmética (es decir, la Aritmética de Peano), pero no definió la multiplicación como total. Esto fue lo suficientemente poderoso (¿lo suficientemente débil?) para negarse a admitir la diagonalización requerida para la prueba de Gödel.

Aparentemente tenía una peculiaridad interesante, que uno podía construir un infinito numerable en un sistema, y ​​luego construir un sistema autorreferencial dentro de él, de tal manera que ese infinito en particular era demostrablemente incontable dentro del "mundo de Willard" autorreferencial, pero demostrablemente numerable. dentro del sistema mayor. Me he divertido jugando con las implicaciones filosóficas que uno podría sacar de eso.

"Todas sus propias declaraciones"??? ¿La negación de un enunciado no sería también un enunciado? ¿Quiere decir que no tiene declaraciones indecidibles porque es demasiado débil para contener toda la aritmética de Peano o viola alguna otra de las suposiciones de Gödel (¿cuál?).
@Conifold Buena captura. Me perdí la palabra "verdadero". Editado para decir que prueba todas sus declaraciones verdaderas. Contiene toda la aritmética de Peano excepto que no garantiza que la multiplicación sea una función total.

Muy, muy simplificado, Gödel mostró cómo se puede expresar el enunciado S "no hay prueba para el enunciado S" en aritmética, y si S es verdadero, entonces tienes un enunciado verdadero sin prueba, o S es falso, entonces tienes un declaración falsa con una prueba. Incompletitud o contradicción.

Obtiene exactamente el mismo resultado en cualquier sistema en el que pueda expresar el mismo enunciado S en el sistema. Ahora puede argumentar razonablemente que los sistemas en los que puede expresar S son más fuertes y aquellos en los que no puede expresar S son más débiles, y se deduce que los sistemas más fuertes son incompletos o contradictorios, mientras que los sistemas más débiles pueden ser completos y sin contradicciones.

¿Qué pasa si introducimos alguna noción alternativa de prueba? ¿Alguien ha estudiado tales sistemas?
El teorema de incompletitud de Gödel y lógicas/sistemas fundacionales no estándar
RespuestasAquíPolítica de privacidad1y, 0v