Como en el teorema de incompletitud de Godel, los números naturales codifican las pruebas de los teoremas. Debido al teorema de completitud de Godel hay un número natural (en algún modelo no estándar) que demuestra $Con(PA)$ .
¿Qué número es? W
Respuestas
¿Demasiados anuncios?
JoshL
Puntos
290
Puedes decir el mismo tipo de cosas que puedes decir sobre cualquier otra prueba codificada. En particular, el número es un código para una secuencia $\langle \phi_1, \ldots, \phi_k\rangle$ de fórmulas tales que $\phi_k$ es $\text{Con}(PA)$ y cada fórmula de la secuencia es un axioma o se obtiene a partir de dos fórmulas anteriores por modus ponens.
Hay dos formas clave en las que la no normalización es relevante:
-
Dado que el modelo no está realmente bien fundado, la "prueba" codificada por un número no estándar puede tampoco estar bien fundada. En otras palabras, podemos tener una fórmula en la prueba que se obtiene por modus ponens a partir de dos fórmulas obtenidas por modus ponens, cada una de las cuales se obtuvo por modus ponens, etc., de modo que si rastreamos hacia atrás nunca llegamos a un axioma en un número finito de pasos. Por supuesto, PA demuestra que "toda fórmula en una prueba codificada se obtiene mediante un número finito de aplicaciones de modus ponens", pero en un modelo no estándar esto puede ser una no estándar número finito de solicitudes.
-
Como el axioma de inducción en PA es un esquema, y como el esquema se representa como una secuencia infinita de fórmulas indexadas con números naturales, en un modelo no estándar hay instancias no estándar del esquema que pueden usarse como axiomas. Por lo tanto, incluso si la prueba estuviera bien fundamentada (en otras palabras, si cada fórmula de la prueba se obtiene a partir de axiomas en un número estándar-finito de aplicaciones del modus ponens), algunos de los axiomas que se utilizan pueden no ser realmente axiomas de PA, porque son instancias no estándar de un esquema de axiomas.
Lo que podemos decir es que, dado que PA es consistente, la prueba codificada de $\text{Con}(PA)$ no puede ser un número estándar. Por lo tanto, uno de los dos puntos anteriores tiene que ocurrir.
dpan
Puntos
3286
No conozco ninguna propiedad específica del "número" que codifica la prueba, pero un análisis básico del tipo de orden de un modelo contable no estándar puede ser bastante esclarecedor.
Lo primero que hay que tener en cuenta es que en el modelo, todos los elementos que son el resultado de la función sucesora sobre 0 se comportan exactamente igual que sus homólogos en el modelo estándar. En otras palabras, el modelo estándar está incrustado en este modelo. Además, es fácil demostrar que es un prefijo del modelo no estándar. Los llamaremos "naturales".
Como este modelo no estándar tiene un elemento que no se comporta como ningún número natural (la prueba Con(PA)), tiene al menos un elemento que es mayor (usando la relación de orden) que todos los "naturales".
Ahora dividimos el modelo según la relación de equivalencia "A es alcanzable desde B usando un número finito de función sucesora (o viceversa)", (equivalentemente - la diferencia entre los dos es un "número natural"). Cada clase de equivalencia tiene la propiedad de orden de N (la primera - que es la "natural"), o de Z (todas las demás), y son "trozos continuos" del orden (ya que los axiomas exigen que cada elemento tenga un sucesor mayor que él; que sólo 0 no tenga un predecesor; y que no haya elementos entre X y S(X)). Por lo tanto, podemos considerar la relación de orden como una relación también entre diferentes clases de equivalencia (ya que se mantendrá para todas las elecciones de representantes de las clases).
Añadiendo cualquier número "no estándar" a sí mismo, es fácil demostrar que hay un número infinito de clases de equivalencia diferentes (obviamente contables - ya que el modelo es contable). Usando la inducción, somos capaces de mostrar que cada dos números tienen una "media" - y promediando números de diferentes clases de equivalencia, obtenemos una clase de equivalencia entre las dos clases. Por lo tanto, la relación de orden, considerada sobre las clases, es una implementación contable de DLO (Dense Linear Order).
Un resultado de Cantor muestra que todo modelo contable de DLO es isomorfo a los racionales. Por lo tanto, el tipo de orden del modelo es equivalente a $\mathbb{N} + \mathbb{Z} \times \mathbb{Q}$ .
