Aritmética de Presburger

Question

La aritmética de Presburger aparentemente demuestra su propia consistencia. ¿Alguien tiene una referencia a una exposición de este? No es claro para mí cómo codificar la instrucción "Presburger la aritmética es consistente" en la aritmética de Presburger.

En la aritmética de Peano esto es posible ya que las funciones recursivas son representables, por lo que un método recursivo de la asignación de los números de Gödel de las fórmulas y de las pruebas significa que la aritmética de Peano puede representar su propia provability relación (de curso, mostrando todo lo que requiere un montón de trabajo). En particular, podemos escribir una aritmética de Peano frase que dice "no hay ningún número natural que codifica una prueba de $\bot$".

Por otro lado, la aritmética de Presburger no puede representar a todas las funciones recursivas. No puede representar a todos los de la primitiva recursiva, de modo que este mismo truco no funciona. Si lo hizo, el primer teorema de la incompletitud, se aplicarían.

Answer 1

La aritmética de Presburger NO probar su propia consistencia. Su única función que los símbolos de suma y sucesor, que no son suficientes para representar a Gödel codificaciones de las proposiciones.

Sin embargo, de acuerdo a la auto-verificación de axioma sistemas existen -- ver el trabajo de Dan Willard ("Auto-Verificación de Axioma Sistemas, el Teorema de la Incompletitud y Relacionados con la Reflexión de Principios"). La idea básica es la de incluir suficientes aritmética para hacer Gödel los códigos de trabajo, pero no lo suficiente para hacer que el teorema de la incompletitud de ir a través de. En particular, se le quita la adición y la multiplicación de los símbolos de la función, y reemplazarlos con la resta y la división. Esto es suficiente para permitir que representa la teoría de la aritméticamente, sino a la totalidad de la multiplicación (el cual es esencial para la prueba del teorema de la incompletitud) no es demostrable, que permite, de manera consistente, añadir una reflexión principio de la lógica.

Answer 2

En tu pregunta dices Aritmética de Presburger "demuestra su propia consistencia". De verdad? Se puede probar consistente, como el artículo de la wikipedia notas, pero no es la prueba se hace en un metalenguaje? Por desgracia estoy en casa durante las vacaciones y no tiene referencias a la mano, pero me gustaría sugerir mirando a Peter Smith "Una Introducción a los Teoremas de Gödel" para empezar a tener claro esto: http://books.google.com/books?id=eK4GmFovS1UC&dq=an+introduction+to+godel%27s+theorems&client=firefox-a&cd=1

Me gusta mucho ese libro. Es en entre Nagel Y Newman exposición popular y la densa presentación se puede encontrar en las matemáticas de la lógica de los textos como de Mendelson. Recuerdo que él específicamente se analiza la aritmética de Presburger y las cuestiones que se plantean aquí.

Answer 3

Presburger presentó su aritmética en 1929 el libro fue traducido al inglés en 1991. Aquí está la cita para este documento:

M. Presburger. Ueber die Vollstaendigkeit eines gewissen Sistemas de der Arithmetik ganzer Zahlen, en cualquiera que sea morir, Además de la ela einzige Operación hervortritt. C. R. du I Congr. des de Matemáticas. des pays Esclavos, Varsovia, 1929, pp 92-101

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

Sobre la integridad de un determinado sistema de la aritmética de los números enteros en la que además se presenta como la única operación Mojżesz Presburger; Dale Jabcquette Historia y Filosofía de la Lógica, 1464-5149, Volumen 12, número 2, 1991, Páginas 225 – 233

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

Él reducción de todas las declaraciones en su aritmética cuantificador libre declaraciones. A ello se agrega para extender el sistema mediante la introducción de modular la equivalencia. El resultado fue una reducción de cada una de las declaraciones para el cuantificador de forma libre. Esto condujo a un algoritmo para decidir cada declaración. De hecho, hay límites en la eficiencia del algoritmo de decisión del algoritmo. Es mayor que el doble exponencial y menos que el triple de exponencial. Para el límite inferior de ver:

M. J. Fischer, M. O. Rabin. Super-Exponencial de la Complejidad de la Aritmética de Presburger. "Actas de la SIAM-AMS Simposio de investigaciones en Matemáticas Aplicadas", 1974, vol. 7, páginas 27-41

Para el límite superior, consulte:

Derek C. Oppen: 2^2^2^pn límite Superior en la Complejidad de la Aritmética de Presburger. J. Comput. Syst. Sci. 16(3): 323-332 (1978)

Para que exista una inconsistencia no tendría que ser un conjunto finito de incoherente modular declaraciones. Debido a esto es posible para mí que el documento original se utiliza el sistema extendido a probar su propia consistencia.

Answer 4

Me gusta el debate. (Actualmente estoy trabajando en temas similares.) He llegado a las siguientes conclusiones. Para que una teoría se puede probar consistente, necesidades o bien (i) se puede probar consistente, pero no por sí mismo, como en Presburger o en Peano, o (ii) se puede probar consistente por sí mismo, pero en ese caso la teoría tiene para no permitir la inferencia a partir de la afirmación de que es consistente con el yo soy mejorables sentencia, como en Willard. La introducción de la reflexión principio es posible precisamente porque de lo que usted dice Adán. Observe que en el caso de que el teorema de punto fijo hizo el trabajo en Willard, esto, en combinación con el principio de reflejo, sería suficiente para que una contradicción, y no importa lo que el estado de el primer teorema de la incompletitud sería.