Antes de hablar de las cuestiones técnicas relacionadas con su pregunta: Sí, para asegurar que una afirmación (sobre los números) es verdadera (en el modelo estándar), actualmente no tenemos ningún procedimiento que no sea exhibir una prueba. (De hecho, la mayoría de los matemáticos argumentarían que ésta es la única manera de discutir significativamente la verdad). Si la afirmación es indemostrable en $\mathsf{PA}$ En el caso de la teoría de conjuntos, dicha prueba por necesidad se encuentra en un sistema más fuerte, típicamente un fragmento de la teoría de conjuntos, $\mathsf{ZFC}$ , a veces un fragmento de aritmética de segundo orden, $\mathsf{Z}_2$ . Pero a veces vamos más allá $\mathsf{ZFC}$ . Las extensiones típicas que consideramos suelen suponer grandes cardenales . Hay un conjunto de pruebas bien justificadas que indican que tiene sentido decir que las pruebas de los enunciados aritméticos en estos sistemas son efectivamente verdaderas (enlazo a una pequeña discusión sobre estos asuntos cerca del final).
(Dado que la prueba está en el centro de esta discusión, puede interesarle una serie de ensayos realizados por informáticos, matemáticos y filósofos, sobre La naturaleza de la prueba matemática que se publicó en la revista Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci, vol 363, No. 1835, 15 de octubre de 2005. Lamentablemente, el único enlace que tengo está detrás de un muro de pago).
Hay una diferencia técnica entre las sentencias producidas por las técnicas de Gödel (o Rosser ') y sentencias como el teorema de Ramsey fuerte que discute el teorema de Paris-Harrington. (Para más ejemplos, véase aquí y las referencias que allí figuran).
La afirmación de Gödel es $\Pi^0_1$ es decir, tiene la forma $\forall n\,\psi(n)$ donde $\psi$ es un enunciado recursivo (en el lenguaje de la aritmética, todos sus cuantificadores están acotados). El teorema fuerte de Ramsey es $\Pi^0_2$ es decir, tiene la forma $\forall n\,\exists m\,\psi(n,m)$ , donde $\psi$ es recursivo.
$\Pi^0_1$ son afirmaciones significativas incluso según los estándares finíticos estrictos (véase, por ejemplo, la obra de Richard Zach disertación y su discusión sobre el análisis de Tait del programa de Hilbert). Son verdaderos si son indemostrables (de hecho, $\mathsf{PA}$ demuestra cada frase $\phi$ que es verdadera para los números naturales y tal que $\lnot\phi$ es $\Pi^0_1$ ): Si $\exists n\,\psi(n)$ es verdadera, entonces para algún número $m$ podemos demostrar esta afirmación simplemente verificando $\psi(m)$ que, al ser una declaración recursiva, tiene una verificación directa - informalmente, ejecutamos un programa de ordenador que está garantizado que se detenga, y comprobamos que el programa produce $\mathtt{Yes}$ .
Por otro lado, $\Pi^0_2$ las afirmaciones no pueden ser calificadas de finitistas. Si son indemostrables, esto no asegura automáticamente su validez (o falsedad). Sin embargo, admiten una interpretación natural: Afirman que cierta función recursiva es total (si la frase es $\forall n\,\exists m\,\psi(n,m)$ la función $f(n)=m$ asigna a cada $n$ lo menos $m$ tal que $\psi(n,m)$ ), es decir, afirman que cierto programa informático se detendrá, sin importar su entrada. Típico de los independientes $\Pi^0_2$ tienen la particularidad de que la función recursiva correspondiente es de crecimiento rápido (véase por ejemplo esta discusión o mi artículo en las secuencias de Goodstein). Por un teorema de Wainer, existe una aproximación matemática estándar para verificar su improbabilidad, a saber, se comprueba que la función $f$ que se discute acaba por dominar la primera $\varepsilon_0$ funciones en una jerarquía de rápido crecimiento.
Se podrían considerar los enunciados de Gödel y similares como enunciados de independencia de primera generación, y los más "combinatorios" $\Pi^0_2$ declaraciones que siguieron como segunda generación. Los argumentos matemáticos implicados en ambos casos son realmente muy diferentes. Una familia de declaraciones de independencia de tercera generación sería $\Pi^0_1$ enunciados combinatorios, por lo que son finitos en el sentido del programa de Hilbert, pero tienen un significado matemático inmediato y aparente (en contraposición con el metamatemático). Esta familia de enunciados se considera de gran interés. Notablemente, el trabajo reciente de Harvey Friedman ha producido ejemplos de este tipo; véase, por ejemplo, su libro sobre la teoría de las relaciones booleanas, disponible en su página .
Esto no es en absoluto el final de la historia. Por ejemplo, ahora tenemos toda una familia de enunciados metamatemáticos independientes de mayor complejidad de los cuales $\mathrm{Con}(\mathsf{PA})$ (la frase del segundo teorema de incompletitud) no es sino la más débil posible. Véase, por ejemplo Aspectos de la Incompletitud de Per Lindström, o Metamatemática de la aritmética de primer orden por Petr Hájek y Pavel Pudlák. En el contexto de la teoría de conjuntos, podemos ir más allá, ya que el teorema de completitud nos dice que la teoría de conjuntos es consistente si y sólo si $\mathrm{Con}(\mathsf{ZFC})$ retenciones. Podemos ir más allá y exigir la existencia de un $\omega$ -(uno cuyo conjunto de números naturales es isomorfo al modelo estándar) o incluso más fuerte, la existencia de un $\beta$ -modelo (es decir, un modelo bien fundado). Woodin ha explicado cómo su $\Omega$ -lógico proporciona, en cierto modo, una extensión última de este proceso.
También tenemos familias de $\Pi^0_2$ afirmaciones cuya verdad es cada vez más difícil de verificar. Por ejemplo, el teorema de Paris-Harrington da un resultado que no sólo es independiente de $\mathsf{PA}$ pero también independiente de la teoría obtenida al añadir a $\mathsf{PA}$ todo cierto $\Pi^0_1$ afirmaciones. Pero es fácil de comprobar una vez que se supera esta teoría. Por otra parte, Friedman identificó una forma finita de Teorema del árbol de Kruskal que no puede ser verificado por los llamados medios predicativos, lo que significa que añadirlo a $\mathsf{PA}$ nos da un sistema con una fuerza de consistencia significativamente mayor que la de $\mathsf{PA}$ con, por ejemplo, el teorema de Goodstein.
Y podemos ir más allá, ya que Friedman tiene ejemplos de $\Pi^0_2$ afirmaciones cuya demostración requiere supuestos de carácter cardinal grande (típicamente, la existencia de cardinales de Mahlo de todos los órdenes finitos, pero los ejemplos recientes van mucho más allá).
En la teoría de conjuntos se estudia la jerarquía de fuerza de consistencia, y se ha identificado una estructura notable, empezando por la identificación de la jerarquía de grandes cardinales. Para una discusión breve y algo técnica de estas cuestiones, véase aquí . La cuestión es que podemos ver estos resultados como una extensión significativa, más allá de la aritmética, del ámbito de lo que es verdadero pero no demostrable (en sistemas formales específicos).
