¿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

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.

Answer 2

El segundo teorema de incompletitud de Gödel da lugar a un curioso ejemplo. El método de diagonalización (como en la demostración del primer teorema de incompletitud) produce, para cualquier teoría razonable T que contenga aritmética (por ejemplo, PA o ZFC), una sentencia S demostrablemente equivalente (en T) a "S es demostrable en T". (A menudo se abrevia tal S como "Soy demostrable en T").

El teorema de Löb dice que este S es de hecho demostrable en T. (Prueba: La teoría T' obtenida de T añadiendo "no S" prueba, por nuestra elección de S, que "S no es demostrable en T", lo que es fácilmente equivalente a la consistencia de T'. Por el segundo teorema de incompletitud de Gödel, T', habiendo demostrado su propia consistencia, debe ser inconsistente. Por lo tanto, T demuestra S).

Nunca he visto un argumento directo para esto, digamos en el caso de PA o de ZFC.

Answer 3

Una buena fuente de ejemplos de este tipo son las teorías decidibles cuyos procedimientos de decisión tienen complejidades computacionales muy elevadas.

Por ejemplo, consideremos la aritmética de Presburger, la teoría de primer orden de la aritmética sin multiplicación. Se puede demostrar que la teoría es decidible (la demostración es sencilla y muy bonita, en mi opinión), lo que significa que cualquier enunciado de la teoría es o bien demostrablemente verdadero o bien demostrablemente falso. Sin embargo, el límite inferior de la complejidad es $2^{2^{\Omega(n)}}$ y los mejores algoritmos realmente conocidos son los triple exponenciales.

Otro ejemplo, que quizá le resulte más convincente desde el punto de vista matemático, es que la teoría de primer orden de los campos reales cerrados también es decidible. (Un corolario de esto es que la teoría de la geometría euclidiana es decidible. Sin embargo, es evidente que la geometría no es trivial. El algoritmo de Tarski tenía una complejidad no elemental, y creo que el límite inferior es doblemente exponencial, aunque desconozco la complejidad de los mejores algoritmos modernos.

EDIT: estos ejemplos son constructivos, en el sentido de que son procedimientos de decisión. Esto puede no ser realmente lo que quieres.

Un ejemplo de prueba de existencia totalmente no constructiva puede encontrarse en la prueba habitual de la completitud de la semántica de Kripke de la lógica intuicionista. Dado que se trata de una prueba clásica, la propiedad de disyunción de la lógica intuicionista (es decir, que $A \vee B$ implica la demostrabilidad de $A$ o la demostrabilidad de $B$ ) se enuncia de forma clásica: la prueba de integridad no proporciona un procedimiento para obtener un disyunto concreto.

Answer 4

Teorema de la imposibilidad de Arrow de la Teoría de la Elección Social, proporciona un ejemplo del tipo de cosas de las que estás hablando:

Concretamente, dice así:

Para un conjunto finito de individuos y alternativas, donde hay al menos tres alternativas, cualquier función de función de bienestar social que satisfaga unanimidad e independencia de alternativas irrelevantes es una dictadura

La prueba puede realizarse en lógica de orden superior, empleando dos inducciones. Aquí se discute una formalización de la prueba en Lógica de Orden Superior, en el asistente informático de pruebas Isabelle: http://www4.informatik.tu-muenchen.de/~nipkow/pubs/arrow.pdf

Aunque el enunciado del teorema es de orden superior, para un número fijo de individuos y un número fijo de alternativas puede expresarse en lógica de primer orden. Utilizando nuestro metateorema de la lógica de orden superior, y la completitud de la lógica de primer orden, sabemos que en principio uno debería ser capaz de demostrar en lógica de primer orden cualquiera de las relativizaciones del teorema de imposibilidad de Arrow...

Pero construir en la práctica una demostración en lógica de primer orden es imposible. Aquí hay un artículo donde el autor proporciona una formulación de primer orden del problema y trató de entregarlo a un teorema prover automatizado: http://staff.science.uva.nl/~grandi/Papers/GrandiEndrissLORI2009.pdf

En resumen, el ordenador produjo una demostración de primer orden del teorema de Arrow relativizado para 2 agentes y tres alternativas en 3 horas, en aproximadamente 200 pasos. El autor utilizó el programa basado en la resolución/paramodulación de primer orden Prover9 y me mencionó que había tenido algo más de éxito con E y Vampiro otros dos sistemas de prueba automatizados. También mencionó que, empíricamente, escalar el problema en cualquiera de los parámetros conducía a un tiempo de computación que crecía más rápido que el exponencial. Así que demostrar el teorema para 100000 individuos y 100000 alternativas en lógica de primer orden está más allá de cualquier persona o máquina.

TL;DR: La completitud de Lógica de Orden Superior/Primer Orden proporciona un metateorema de que todas las instancias de primer orden de Teorema de la imposibilidad de Arrow debe ser demostrable en lógica de primer orden, pero en la práctica producir una demostración de primer orden es transcomputable.

Answer 5

Esto es casi un resultado del tipo que el OP quería: En su intento de demostrar lo que ahora se conoce como el teorema de los números primos, Chebyshev utilizó un argumento elemental que implicaba una secuencia finita de pesos numéricos inteligentemente elegida para demostrar que el número de números primos hasta $x$ está entre $0.92 x/\log x$ y $1.11 x/\log x$ para grandes $x$ . Es natural preguntarse si el método de Chebyshev puede ampliarse para acercarse al teorema del número primo. Rosser y Erdos-Kalmar demostraron de forma independiente que para cualquier $\varepsilon>0$ existía una secuencia de pesos para la que el método elemental de Chebyshev demostraba que el número de primos hasta $x$ entre $(1-\varepsilon) x/\log x$ y $(1+\varepsilon) x/\log x$ . Envío de $\varepsilon \to 0$ ¡parecería una prueba elemental de la PNT! Pero hay una trampa muy importante: los argumentos de Rosser y Erdos-Kalmar utilizan la PNT en la demostración (y en aquel momento no se conocía ninguna demostración elemental de la PNT). Así que tenemos una prueba no elemental de que existen pruebas elementales de (aproximaciones arbitrarias a) la PNT. Véase el capítulo 9 de

Harold G. Diamond MR 670132 Métodos elementales en el estudio de la distribución de los números primos , Bull. Amer. Math. Soc. (N.S.) 7 (1982), no. 3, 553--589.

para seguir debatiendo.

Resulta que este resultado en particular no responde del todo a la pregunta original, porque puede hacerse constructivo: las regiones libres de cero de zeta establecidas numéricamente pueden convertirse constructivamente en pruebas elementales de la PNT con una pérdida de épsilon. Pero al menos es un ejemplo de un metateorema no elemental sobre la existencia de pruebas elementales.