¿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

El teorema de Jacobson de que los anillos X^m = X son conmutativos proporciona un ejemplo esclarecedor, véase mi post a continuación para más discusión y referencias
Pensamiento abstracto frente a cálculo

Answer 2

No estoy seguro del papel de la palabra "no constructivo" en su pregunta. A ver si lo siguiente le aporta algo:

A veces es más fácil demostrar que algo es cierto en todos los modelos que probarlo.

En la teoría de topos, para ciertas teorías de primer orden ("teorías geométricas") se tiene un modelo genérico, cualquier otro modelo en cualquier otro topos (incluida la categoría de conjuntos) es una imagen del modelo genérico bajo un mapa, que preserva la validez de las fórmulas geométricas. De modo que si se puede demostrar que una determinada fórmula geométrica es cierta para el modelo genérico, entonces es cierta en cualquier modelo dado. A menudo, mostrar algo sobre el modelo genérico equivale a exponer una prueba, porque en general la única descripción que se tiene es como modelo sintáctico. Pero si tenemos, digamos, un anillo local dado (=un modelo para la teoría geométrica de anillos locales en el topos de conjuntos), y demostramos una afirmación geométrica sobre el anillo local genérico, entonces sabemos que es cierta en nuestro anillo local dado sin haber proporcionado una demostración. Puesto que tenemos una descripción directa del anillo local genérico como un functor (es decir, no sólo como un modelo sintáctico), se pueden utilizar métodos no constructivos para la demostración.

Muy relacionada está la afirmación de que, para alguna teoría geométrica T, una afirmación geométrica es válida para cada modelo de T en cada topos si es válida para cada modelo en Conjuntos (véase la última página, antes del apéndice, de Moerdijk/MacLane ). Siguiendo con el ejemplo anterior, puedes demostrar un teorema sobre anillos locales (es decir, anillos locales habituales en conjuntos), utilizando el axioma de elección y lo que quieras, y luego deducir que debe ser cierto, por ejemplo, para gavillas de anillos con anillos locales como tallos (es decir, objetos de anillos locales en un topos de gavillas), siempre que la afirmación tenga la forma sintáctica correcta, es decir, geométrica. Según la completitud de la teoría de topos, debe existir una prueba (constructiva), pero la has deducido ahora sin mostrarla.

Answer 3

El ejemplo más comprensible de lo que pide el remitente, a mi juicio, es la "dualidad" en Geometría Proyectiva: Para cualquier teorema y su demostración, existe un teorema y una demostración "duales", derivados del teorema/la demostración dados intercambiando los términos "punto" y "línea" en todas partes.