Aritmética Presburger

Question

La aritmética de Presburger demuestra aparentemente su propia consistencia. ¿Alguien tiene una referencia a una exposición de esto? No me queda claro cómo codificar la afirmación "la aritmética de Presburgo es consistente" en la aritmética de Presburgo.

En la aritmética de Peano esto es posible ya que las funciones recursivas son representables, por lo que un método recursivo para asignar números de Godel a fórmulas y pruebas significa que la aritmética de Peano puede representar su propia relación de demostrabilidad (por supuesto, demostrar todo esto requiere mucho trabajo). En particular, podemos escribir una sentencia aritmética de Peano que diga "no hay ningún número natural que codifique una prueba de $\bot$ ".

Por otra parte, la aritmética de Presburgo no puede representar todas las funciones recursivas. Ni siquiera puede representar todas las recursivas primitivas, por lo que este mismo truco no funciona. Si lo hiciera, se aplicaría el primer teorema de incompletitud.

Answer 1

La aritmética de Presburger NO demuestra su propia consistencia. Sus únicos símbolos de función son la suma y el sucesor, que no son suficientes para representar las codificaciones de Godel de las proposiciones.

Sin embargo, existen sistemas axiomáticos autoverificables coherentes: véase el trabajo de Dan Willard ( "Sistemas de axiomas autoverificables, el teorema de incompletitud y principios de reflexión relacionados" ). La idea básica es incluir suficiente aritmética para que funcionen las codificaciones de Godel, pero no la suficiente para que se cumpla el teorema de incompletitud. En concreto, se eliminan los símbolos de las funciones de suma y multiplicación, y se sustituyen por los de resta y división. Esto es suficiente para permitir representar la teoría aritméticamente, pero la totalidad de la multiplicación (que es esencial para la demostración del teorema de incompletitud) no es demostrable, lo que le permite añadir coherentemente un principio de reflexión a la lógica.

Answer 2

En su pregunta dice que la Aritmética de Presburgo "demuestra su propia consistencia". ¿Realmente? Es demostrablemente consistente, como señala el artículo de la wikipedia, pero ¿no se demuestra en un metalenguaje? Desgraciadamente, estoy en casa de vacaciones y no tengo referencias a mano, pero sugeriría consultar "An Introduction to Godel's Theorems" de Peter Smith para empezar a entender estas cosas: http://books.google.com/books?id=eK4GmFovS1UC&dq=an+introduction+to+godel%27s+theorems&client=firefox-a&cd=1

Me gusta mucho ese libro. Está entre la exposición popular de Nagel y Newman y la presentación densa que se encuentra en textos de lógica matemática como el de Mendelson. Recuerdo que discute específicamente la aritmética de Presburger y las cuestiones que planteas aquí.

Answer 3

Presburger presentó su aritmética en 1929 y el artículo se tradujo al inglés en 1991. Aquí está la cita de este documento:

M. Presburger. Sobre la completitud de cierto sistema de aritmética de los números enteros, en el que destaca la suma como única operación. C.R. du I Congr. des Math. des pays Slaves, Varsovia, 1929, pp.92-101

Aquí está la traducción al inglés:

Sobre la completitud de cierto sistema aritmético de números enteros en el que la suma es la única operación Mojżesz Presburger; Dale Jabcquette Historia y filosofía de la lógica, 1464-5149, Volume 12, Issue 2, 1991, Pages 225 - 233

El pdf aquí que se menciona en el comentario de Jason Dyer a la pregunta original afirma que en el documento anterior el sistema se utiliza para demostrar su propia consistencia.

Redujo todos los enunciados de su aritmética a enunciados sin cuantificador. Para ello, amplió el sistema introduciendo la equivalencia modular. El resultado fue una reducción de cada enunciado a la forma libre de cuantificador. Esto condujo a un algoritmo para decidir cada enunciado. De hecho, hay límites en la eficiencia del algoritmo de decisión. Es mayor que el doble exponencial y menor que el triple exponencial. Para el límite inferior ver:

M. J. Fischer, M. O. Rabin. Super-Exponential Complexity of Presburger Arithmetic. "Proceedings of the SIAM-AMS Symposium in Applied Mathematics", 1974, vol. 7, pp.27-41

Para el límite superior, véase:

Derek C. Oppen: A 2^2^2^pn Upper Bound on the Complexity of Presburger Arithmetic. J. Comput. Syst. Sci. 16(3): 323-332 (1978)

Para que haya incoherencia tendría que haber un conjunto finito de enunciados modulares incoherentes. Por eso me parece plausible que el artículo original utilizara el sistema ampliado para demostrar su propia consistencia.

Answer 4

Me gusta la discusión. (Actualmente estoy trabajando en temas similares.) He llegado a las siguientes conclusiones. Para que una teoría sea demostrablemente consistente, necesita o (i) ser demostrablemente consistente pero no por sí misma, como en Presburger o en Peano, o (ii) ser demostrablemente consistente por sí misma pero en ese caso la teoría tiene que desautorizar la inferencia desde la afirmación de que es consistente hasta el Soy mejorable sentencia, como en Willard. La introducción del principio de reflexión es posible allí exactamente por lo que dices Adam. Fíjate que en caso de que el teorema del punto fijo funcionara en Willard, esto, en combinación con el principio de reflexión, bastaría para una contradicción, y no importaría cuál fuera el estatus del primer teorema de incompletitud.