Descargo de responsabilidad: No soy un experto en la teoría de la prueba de la aritmética. Sin embargo, no creo que sea necesario serlo para evaluar este documento. Es admirablemente claro, bien escrito y bien referenciado, por lo que no es difícil verificar que sus afirmaciones matemáticas precisas y pruebas parecen perfectamente correctas, y no particularmente controversiales. Sin embargo, su principal afirmación extra-matemática, que estos resultados pueden ser considerados como una prueba de la consistencia de PA, formalizable en PA, parece poco convincente, y sus argumentos para esta afirmación no son, en mi opinión, particularmente novedosos (aunque Artemov los presenta de manera inusualmente clara).
Las principales afirmaciones matemáticas precisas son (paráfrasis muy ligera):
- para cada $n$, PA demuestra la afirmación " $n$ no codifica una prueba de $\bot$ en PA" (que abreviamos como "$\lnot (n \colon \bot)$");
- además, esto es demostrado por una función recursiva primitiva que toma cada $n$ como la prueba de "$\lnot (n \colon \bot)$";
- estos dos hechos pueden ser demostrados en PA.
Los dos primeros hechos se pueden demostrar de manera bastante directa utilizando técnicas estándar de la teoría de la prueba de la aritmética, de varias formas (Artemov utiliza definiciones de verdad para fórmulas $\Sigma_n$); y el hecho de que PA sea una metateoría suficiente para ellos (de hecho, fragmentos pequeños como PRA son suficientes) también es estándar, como se discute en, por ejemplo, las respuestas de esta antigua pregunta de MO. No hay nada controvertido o cuestionable sobre esto.
El paso tenue es cuando Artemov argumenta que esto puede verse como una prueba de la consistencia de PA, dentro de PA. La estirada se hace clara cuando desglosamos cuidadosamente la afirmación en definiciones. "PA es consistente" significa "no hay una prueba de contradicción en PA", es decir, "no hay un $n$ que codifique una prueba de $\bot$ en PA", o equivalentemente "para cada $n$, $n$ no codifica una demostración en PA de $\bot$". Entonces, simplemente considerando que las cosas significan lo que se definen, una prueba de "PA es consistente" en PA debería ser una prueba de "para todo $n$, $\lnot (n \colon \bot)$" en PA.
Artemov argumenta que dado que para cada $n$ podemos probar "$\lnot (n \colon \bot)$" en PA, y podemos demostrar esa probabilidad esquemática usando PA como metateoría, podemos ver esto en su conjunto como una prueba de la consistencia de PA en PA. Pero hay que tener en cuenta que el cuantificador "para cada $n$" se ha movido entre la afirmación de probabilidad. Por lo tanto, hemos demostrado en el PA interno un esquema de afirmaciones, y luego en el PA externo, podemos afirmar la demostrabilidad de ese esquema como una sola afirmación. Pero no hemos presentado una prueba en ninguno de los dos PA de una sola afirmación que pueda interpretarse como "PA es consistente". En el PA interno, hemos probado un esquema de afirmaciones sobre derivaciones finitas específicas en PA. En el PA externo, hemos demostrado un hecho sobre PA que ciertamente no se puede interpretar como "PA es consistente", ya que podríamos probar el mismo esquema para una teoría inconsistente de la aritmética. El argumento de Artemov de que esto se puede llamar una prueba en PA de la consistencia de PA me recuerda a un viejo chiste: "Si llamas a la cola de un perro una pata, ¿cuántas patas tiene un perro?" "Cuatro: llamar a la cola una pata no significa que lo sea".
La prueba paramétrica de este esquema ciertamente muestra que PA está muy cerca de demostrar su propia consistencia. Un argumento similar para ZF puede darse, por ejemplo, mediante el teorema de reflexión: que para cualquier lista finita de axiomas de ZF, ZF demuestra que hay algún $V_\alpha$ que los modela (y por lo tanto que son consistentes). La mayoría de las presentaciones de estos principios de reflexión que he visto discuten este punto explícitamente, señalando que estos resultados acercan mucho a la teoría a demostrar su propia consistencia, pero en inspección detallada, no lo prueban del todo.
Un punto de fondo que vale la pena señalar aquí (un punto que, si mal no recuerdo, aprendí de Timothy Chow en este sitio) es que el programa de consistencia de Hilbert no era simplemente probar la consistencia de la aritmética dentro de la aritmética, ya que ese sería un resultado bastante débil, ya que una teoría inconsistente seguiría demostrando su propia consistencia. La esperanza de Hilbert era probar la consistencia de algún tipo de teoría de conjuntos a partir de alguna teoría de la aritmética, justificando una teoría más abstracta mediante una más autoevidente, lo que sería un resultado genuinamente valioso. El punto del teorema de Gödel fue mostrar que ni siquiera el resultado mucho más débil era alcanzable, y mucho menos el resultado más fuerte que Hilbert esperaba. Por lo tanto, si bien los argumentos del principio de reflexión muestran que PA y ZF están al borde de demostrar su propia consistencia, lo suficientemente cerca como para que un poco de buena retórica se estire tenuemente a través del espacio, no se acercan en absoluto al sueño real de Hilbert, de probar la consistencia de la teoría de conjuntos a partir de la aritmética; y según Gödel, no pueden, ya que fragmentos finitos de teoría de conjuntos son suficientes para probar la consistencia de PA.
