¿Existen buenos "metateoremas existenciales" no constructivos?

Question

¿Existen buenos ejemplos de teoremas en teorías razonablemente expresivas (como la aritmética de Peano) para los que sea sustancialmente más fácil demostrar (en una metateoría) que existe una demostración que encontrar realmente la demostración? Cuando digo "sustancialmente más fácil", no hay que tener en cuenta lo tedioso que resulta formalizar una prueba informal. En otras palabras, una prueba rigurosa pero informal no cuenta como demostración no constructiva de que existe una prueba formal, ya que no hay ninguna dificultad esencial para producir una prueba formal aparte de la carga de trabajo. Si hay alguna barrera esencial, entonces hay algo mal o con la prueba o con la definición de "prueba formal". (Aunque el concepto de "prueba informal" es por naturaleza vago, parece razonable decir que el procedimiento que transforma una prueba informal típica en una prueba formal es un cálculo recursivo primitivo, aunque probablemente sea imposible hacerlo lo suficientemente preciso como para demostrarlo).

No sé cómo podría ser una metaprueba no constructiva, pero tampoco veo por qué no podría existir. El único ejemplo cercano que se me ocurre ahora mismo está en el cálculo proposicional: se puede demostrar que una fórmula proposicional es un teorema comprobando su tabla de verdad, que no proporciona explícitamente una deducción a partir de los axiomas; sin embargo, en la mayoría de los casos interesantes, eso probablemente no sea mucho más fácil (si es que lo es) que exponer una prueba, sólo quizá más mecánico. (Por supuesto, estimar la dificultad de demostrar o refutar un candidato a teorema proposicional es un enorme problema abierto). Además, creo que en realidad hay una forma sencilla de convertir una prueba de tabla de verdad en una deducción real a partir de los axiomas del cálculo proposicional, aunque no lo recuerdo y no repasé todos los detalles. (De todos modos, ni siquiera estoy tan interesado en el cálculo proposicional para esta cuestión, ya que no es muy expresivo).

Otra cosa que parece vagamente relevante es el teorema de completitud de Godel, que afirma que una fórmula es un teorema de una teoría de primer orden si y sólo si es verdadera en cada modelo de esa teoría. Sin embargo, no sé en qué casos sería más fácil demostrar que alguna fórmula es cierta en todos los modelos que demostrar el teorema en la teoría.

Answer 1

Eh, esto es más bien un "metaalgoritmo existencial", pero creo que quizá merezca la pena mencionarlo...

Una consecuencia del teorema del grafo menor de Robertson-Seymour es que, para cualquier superficie dada, existe un algoritmo de tiempo polinómico (¡en realidad de tiempo cúbico!) para decidir si se puede dibujar un grafo en esa superficie. Pero este algoritmo no es explícito, ya que se basa en probar un número finito pero no limitado de grafos para ver si son menores que el grafo de entrada. En realidad, hasta donde yo sé, ni siquiera podemos describir este algoritmo para comprobar si un grafo es incrustable en un toro - ¡y se sabe que calcular el género del grafo en general es NP-completo! Así que sabemos que existe un algoritmo "eficiente", aunque su descripción es conocida (suponiendo que P \neq NP) ser duro.

Answer 2

La teoría de conjuntos es un buen ejemplo. En la teoría de conjuntos suele ser conveniente trabajar con el concepto de "clases" y tratarlas como objetos matemáticos propios. La axiomatización estándar de la teoría de conjuntos con clases se denomina teoría de conjuntos de Goedel-Bernays, denominada GBC, mientras que los axiomas habituales de ZFC sólo tienen objetos conjuntos. Pero existe un teorema general según el cual cualquier afirmación puramente sobre conjuntos que se demuestre utilizando clases en GBC puede demostrarse sin ellas puramente en ZFC. Esto es lo que significa decir que GBC es una conservador extensión de ZFC. Para demostrar este teorema general, basta observar que cualquier modelo de ZFC puede expandirse a un modelo de GBC, añadiendo únicamente las clases definibles a partir de parámetros.

Hay muchos otros ejemplos de extensiones conservativas en matemáticas, y todos ellos parecerían ser ejemplos del tipo que buscas. Por ejemplo, PA tiene una extensión conservativa a la teoría análoga verdadera en la colección HF de conjuntos hereditariamente finitos. Así, para demostrar un teorema sobre números en PA, uno puede utilizar libremente conjuntos hereditariamente finitos (por ejemplo, secuencias de números, secuencias de conjuntos de números, etc.), no sólo como codificados por números mediante la codificación de Goedel, sino como objetos matemáticos reales. Y sin duda esto facilita mucho las demostraciones.

Quizás otro tipo de ejemplo surge en el fenómeno de la absolutidad en la teoría de conjuntos. Por ejemplo, el El teorema de Shoenfield afirma que cualquier afirmación Sigma^1_2 tiene el mismo valor de verdad en dos modelos cualesquiera de teoría de conjuntos con los mismos ordinales. En particular, para demostrar que un enunciado Sigma^1_2 concreto es verdadero en ZFC, basta con demostrarlo bajo el supuesto también de que V=L, donde también se dispone de todo tipo de estructura adicional. Por lo tanto, los teoremas absolutos (y hay muchos) pueden verse bajo la rúbrica que mencionas.

Pero, por supuesto, en todos estos casos, tenemos una prueba real en la teoría más débil. Demostrar que hay una prueba, es una prueba, así que creo que, en última instancia, no habrá manera de evitar las disputas sobre si es fácil o difícil traducir la prueba de alto nivel en una prueba de bajo nivel, ya que, en principio, siempre será posible hacerlo.

Answer 3

Harvey Friedman tiene un ejemplo de enunciado finito (que en realidad es "finito" y no "finitario", es decir, $\Pi_0^0$ en lugar de $\Pi^0_1$ ) que tiene una demostración, usando axiomas cardinales grandes, que no tiene más de un millón de símbolos de longitud, pero cuya demostración en ZFC con abreviaturas debe contener más de $10^{1000}$ símbolos. Obviamente, "encontrar" explícitamente la prueba ZFC es totalmente inviable. Véase el último teorema (teorema 5) en esta entrada a la lista de correo de Fundamentos de Matemáticas.

En cierto sentido, la inviabilidad computacional es el único tipo de obstáculo que puede existir aquí. Si existe una prueba, entonces se puede encontrar mediante una búsqueda exhaustiva, por lo que no puede haber un argumento no constructivo para la existencia de una prueba en el sentido fuerte de un argumento que te da ningún algoritmo para encontrar la prueba. Así pues, en cierta medida, el ejemplo de Friedman es el ejemplo más sólido que se puede esperar.

Answer 4

Esto no es exactamente lo que plantea la pregunta original, pero ciertamente en informática hay muchos problemas que se pueden resolver rápidamente mediante un argumento probabilístico, pero no se conoce ningún algoritmo determinista (el problema P=BPP, básicamente). Por ejemplo, consideremos la tarea de decidir si una identidad polinómica en muchas variables sobre un campo finito fijo es cierta. Se puede decidir esto con una probabilidad arbitrariamente alta rápidamente, simplemente probando asignaciones aleatorias de las variables y viendo si alguna vez se obtiene un contraejemplo. (El Lema de Schwarz-Zippel nos dice que si la identidad falla, entonces falla un lote y, por tanto, se recogerá con alta probabilidad mediante muestreo aleatorio).

Por tanto, si una identidad polinómica es cierta, uno puede convencerse rápidamente de que lo es, pero esto no da ninguna pista sobre cómo encontrar una prueba formal de que la identidad es cierta, a menos que se evalúen todas y cada una de las opciones de asignación, o se expanda la identidad por completo y se comparen los coeficientes (lo que, en realidad, acaba suponiendo más o menos la misma cantidad de trabajo (es decir, exponencial en la dimensión)).

Answer 5

Un principio básico de la lógica de primer orden es que, si un teorema se deduce de una lista de axiomas, entonces se deduce de algún subconjunto finito de esa lista. Esto puede dar lugar a consecuencias no triviales. Por ejemplo:

(1) Si $T$ es cualquier afirmación verdadera de primer orden sobre campos de característica cero, entonces existe una constante $N$ para que $T$ es cierta para campos de característica $>N$ .

Prueba: tome su lista de axiomas como los axiomas de campo estándar más, en el caso (1), el axioma $1+1+1+\cdots+1 \neq 0$ donde la suma es sobre $p$ unos por cada primo $p$ .

Un ejemplo similar es:

(2) Si $T$ es cualquier enunciado verdadero de primer orden sobre campos algebraicamente cerrados, existe una constante $N$ tal que $T$ es cierto para cualquier campo $K$ en el que cada polinomio de grado $\leq N$ tiene una raíz.

En ambos casos, puede ser más fácil demostrar (informalmente) un resultado sobre la característica cero/campos algebraicamente cerrados que extraer la constante $N$ .

He aquí otro ejemplo. Recordemos que el teorema de Ramsey (en un caso especial) dice:

(3) Para cualquier número entero positivo $N$ existe un número entero $M$ tal que, para cualquier bicoloración del grafo completo en $M$ vértices, existe un subgrafo completo monocromático en $N$ vértices.

Según tengo entendido, la prueba original era demostrar

(3') Para cualquier bicoloración del grafo completo en infinitos vértices, existe un subgrafo completo infinito monocromático.

Esto implica claramente

(3'') Para cualquier número entero positivo $N$ y cualquier bicoloración del grafo completo en infinitos vértices, existe un subgrafo completo monocromático en $N$ vértices.

Escribiendo (3'') formalmente, se termina con una secuencia infinita de axiomas, diciendo que el gráfico tiene más de $k$ vértices para cada $k$ . Dado que en la demostración de (3'') sólo se utilizan un número finito de esos axiomas, vemos que (3) debe cumplirse. Por supuesto, ahora hay pruebas directas de (3), pero creo que la prueba de la teoría lógica fue la primera.