resultados de complejidad no asintótica

Question

Recuerdo haber oído hablar de un resultado, o tal vez un grupo de resultados, en algún área de la teoría de la complejidad, probablemente algebraica, en el sentido de que hay fórmulas conocidas, específicas y cortas, cuya derivación mínima se sabe que es excesivamente larga. O tal vez se trate de una función específica que requiere un circuito excesivamente profundo. La "filosofía" parecía ser que tales ejemplos amenazarían con hacer obsoleta la antigua cuestión asintótica: "A quién le importa la asintótica si las constantes son enormes". ¿Puede alguien, dadas estas pistas, describir ( y dirigirme a) el resultado que escuché?

Answer 1

Establecer que las pruebas mínimas (o "derivaciones") de ciertos enunciados o teoremas son largas, es el objetivo principal del área llamada complejidad de la prueba . En cuanto a los ejemplos dados en las respuestas anteriores, como el límite inferior del tamaño de Haken en las pruebas del principio de casillero, tratan de lógica proposicional solamente. Por lo tanto, son asintótica resultados de la forma: "existe una constante $ 0<\epsilon<1 $ tal que cualquier refutación de resolución del principio proposicional de pigenohole $ PHP_n$ debe tener una longitud (es decir, un número de pasos) de al menos $ 2^{n^\epsilon}$ "; Donde $ PHP_n \;$ , $ n=1,2,\ldots ,$ es una familia infinita de contradicciones proposicionales (que expresan la $ n+ 1 $ a $ n\; $ principio de encasillamiento). Así que la complejidad de la prueba proposicional no parece responder a la pregunta sobre los límites inferiores no asintóticos.

Por otro lado, los límites inferiores de primera orden Las pruebas (que tienen cuantificadores, es decir, que no son de lógica proposicional) no son necesariamente asintóticas, y si esto es lo que está buscando, el único estudio exhaustivo que conozco (que trata tanto de la complejidad de las pruebas proposicionales como de las no proposicionales) es: Pavel Pudlak: The lengths of proofs, en Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637 , disponible aquí

(También hay un libro más antiguo de Orevkov sobre la complejidad de las pruebas no proposicionales: [1993] Complexity of Proofs and Their Transformations in Axiomatic theories, vol. 128 de Translations of Mathematical Monographs, American Mathematical Society, Providence, Rhode Island).

Answer 2

He encontrado una cita de este documento de Joel Spencer: "Teoremas cortos con pruebas largas" [ Amer. Math. Monthly 90 (6) 365-366 (1983)]. Pero no tengo acceso a ella en este momento. Desde luego, el título parece relevante.

Editar . Pero aparentemente, no según el comentario de michael El resumen de este trabajo de Marian Mrozek, " Propiedades heredables y pruebas asistidas por ordenador en dinámica " dice

Dado que existen teoremas cortos con pruebas arbitrariamente largas (una consecuencia de la incompletitud de G "odel de G "odel, ver [4, 6, 23]) ...

La referencia [4] es el documento de Spencer. Así que supongo que esto sólo confirma que esto es de conocimiento común, sin proporcionar el ejemplo explícito que buscas. Disculpas por la distracción.