Profundos teoremas y largo pruebas

Question

Corrí a través de esta discusión por Daniel Mangos,

"Es la ley de la reciprocidad cuadrática una profunda teorema?." Resueltos y sin resolver los Problemas de Teoría de números. Vol. 297. AMS, 2001. p.64ff.

que me hizo preguntarme:

Q. Hay un teorema en algún sistema formal cuyas pruebas son conocidos por ser necesariamente "largo" en algún sentido, tal vez en el test de Kolmogorov-complejidad sentido?

Sé que se ha establecido que hay relativamente "corto" teoremas que han sólo enormemente "de largo" pruebas (al parecer[?] debido a Gödel,"Sobre la duración de las pruebas"), pero estoy preguntando si se sabe que algunos en particular el teorema de sólo ha de largo pruebas? (Este es, en cierto sentido, el anverso de la MO compendio, "Rápida pruebas de duro teoremas.")

Obviamente esta es una pregunta ingenua!

Answer 1

Si usted está dispuesto a aceptar un artificioso declaración, entonces no es difícil obtener una muestra explícita, pero esto puede no ser la clase de ejemplo que usted está buscando.

Siguiente Gödel enfoque, usted puede hacer una declaración de la forma "yo no tengo ninguna prueba formal de menos de cien páginas." (Más exactamente, usted debe utilizar implícita la auto referencia, a lo largo de las líneas de "no Hay ninguna prueba formal de menos de cien páginas de esta cadena seguida de su cita:" no Hay ninguna prueba formal de menos de cien páginas de esta cadena seguida de su cita:'")

Suponiendo que el sistema formal es consistente, esta declaración no puede ser probado en menos de cien páginas. En ese caso, lo que realmente es demostrable, porque se puede demostrar mediante la enumeración de todos los posibles pruebas de menos de un centenar de páginas y comprobar que no funcionan. Así, tenemos un relativamente corto teorema que no tiene corto de prueba formal. Lamentablemente, el teorema es de ningún interés intrínseco.

Tenga en cuenta que la razón por la que no nos tome de un centenar de páginas para probar el teorema es porque asumimos que el sistema formal fue constante. Por Gödel del segundo teorema de la incompletitud, el sistema no puede probar su propia consistencia, por lo que este enfoque no está disponible en el sistema. De hecho, este argumento prueba que el segundo teorema de la incompletitud: si la consistencia tuvo una corta prueba suficiente, entonces se podría llevar a cabo este argumento para probar el teorema en menos de cien páginas. No hay nada especial acerca de un centenar de páginas en este argumento, por lo que no hay prueba de la consistencia de todas. Este enfoque para el segundo teorema de la incompletitud es fundamentalmente el mismo que Gödel de la prueba original.

Aquí he sido la medición de las pruebas por la longitud, en lugar de la complejidad de Kolmogorov menciona en la pregunta. Eso no es una medida útil para las pruebas, porque se puede reconstruir la menor prueba de teorema de X en el sistema S de poco más de X y una prueba de corrector para S (que se puede aplicar para hacer una búsqueda por fuerza bruta, y por el menor prueba). Esto significa que si usted fijar S, la prueba de Kolmogorov complejidad de la más corta de la prueba no es más que una constante aditiva mayor que la del teorema de sí mismo.

Answer 2

Hay un cuerpo de trabajo muy interesante que rodea la prueba de la complejidad de las diversas formulaciones de la conocida pigeon-hole principio, el hecho de que no hay ninguna función inyectiva de un conjunto de tamaño $m$ a un conjunto de tamaño $n$, cuando se $m\gt n$. Resulta que a la dificultad de probar esto depende de la cantidad más grande de $m$ es de $n$, y así en la actualidad disponemos de una gran variedad de pigeon-hole principios aquí:

• Pigeon-hole principio. No es inyectiva mapa de $n+1\to n$ para los números naturales $n$.

• Moderadamente débil pigeon-hole principio. No hay inyección de $2n\to n$, para los positivos números naturales $n$.

• Débil pigeon-hole principio. No hay inyección de $n^2\to n$ para los números naturales $n>1$.

• Muy débil de la paloma-sostenga el principio. No hay inyección de $\infty\to n$, para cualquier finito $n$.

Los principios se vuelven más fáciles de probar, por supuesto, como el dominio se hace más grande, y no son más cortas pruebas cuando el dominio es muy grande. El papel de la Prueba de la complejidad de pigeon-hole principios por Alexander Rozborov contiene interesantes resultados en la prueba computacional de la complejidad de estas diversas formulaciones de la paloma-agujero principio, y, en particular, de la necesaria largas longitudes de pruebas en ciertos sistemas. Mientras tanto, los resultados de Sam Buss, el Polinomio de tamaño pruebas de la proposicional pigeon-hole principio muestran que existe una dependencia en particular, la prueba del sistema que se adopte, ya que en ciertas Frege sistema uno todavía puede obtener el polinomio de tamaño de pruebas.