¿Qué teoremas interesantes en TCS se basan en el Axioma de elección? (¿O, alternativamente, el Axioma de la Determinación?)

67

Los matemáticos a veces se preocupan por el Axioma de Elección (AC) y el Axioma de Determinación (AD).

Axioma de elección : Dado cualquier colección de conjuntos no vacíos, hay una función f que, dado un conjunto S en C , devuelve un miembro de S .CfSCS

Axioma de Determinación : Sea un conjunto de cadenas de bits infinitamente largas. Alice y Bob juegan un juego en el que Alice elige un primer bit b 1 , Bob elige un segundo bit b 2 , y así sucesivamente, hasta que se construye una cadena infinita x = b 1 b 2 . Alice gana el juego si x S , Bob gana el juego si x S . La suposición es que para cada S , hay una estrategia ganadora para uno de los jugadores. (Por ejemplo, si S consiste solo en la cadena de todos, Bob puede ganar en muchos movimientos finitos).Sb1b2x=b1b2xSxS SS

Se sabe que estos dos axiomas son inconsistentes entre sí. (Piénsalo o ve aquí ).

Otros matemáticos prestan poca o ninguna atención al uso de estos axiomas en una prueba. Parecen ser casi irrelevantes para la informática teórica, ya que creemos que trabajamos principalmente con objetos finitos. Sin embargo, debido a que TCS define los problemas de decisión computacional como cadenas de bits infinitas, y medimos (por ejemplo) la complejidad temporal de un algoritmo como una función asintótica sobre los naturales, siempre existe la posibilidad de que el uso de uno de estos axiomas pueda arrastrarse en algunas pruebas.

¿Cuál es el ejemplo más sorprendente en TCS que sabes dónde se requiere uno de estos axiomas ? (¿Conoces algún ejemplo?)

Solo para presagiar un poco, tenga en cuenta que un argumento de diagonalización (sobre el conjunto de todas las máquinas de Turing, por ejemplo) no es una aplicación del Axioma de Elección. Aunque el lenguaje que define una máquina de Turing es una cadena de bits infinita, cada máquina de Turing tiene una descripción finita, por lo que realmente no necesitamos una función de elección para infinitos conjuntos infinitos aquí.

(Puse muchas etiquetas porque no tengo idea de dónde vendrán los ejemplos).

Ryan Williams
fuente
CW? o no ? no es seguro.
Suresh Venkat
Tampoco estoy seguro ... esta es una pregunta en la que estoy muy inseguro sobre la "complejidad" de la respuesta ...
Ryan Williams
55
Otros matemáticos prestan poca o ninguna atención al uso de estos axiomas en una prueba. ¿Los matemáticos realmente usan ambos axiomas descuidadamente? Si accidentalmente asumes ambos axiomas, ¡puedes probar cualquier cosa!
Warren Schudy
1
Conjetura de Harvey Friedman . No sé si también se aplica a la informática teórica.
Kaveh
1
No conozco ningún resultado en la informática teórica que no se pueda probar en ZF pero se pueda probar en alguna extensión interesante de ZF. Dicho esto, mi conjetura es que incluso esos resultados probablemente no requerirán el axioma de elección completo (AC) y que solo requieren alguna versión más débil de AC como el axioma de elección dependiente (DC) o el axioma aún más débil de contable elección (AC_ω). Por otro lado, DC (y por lo tanto AC_ω) es consistente con el axioma de determinación .
Tsuyoshi Ito

Respuestas:

47

Cualquier declaración aritmética demostrable en ZFC es demostrable en ZF, y por lo tanto no "necesita" el axioma de elección. Por una declaración "aritmética" me refiero a una declaración en el lenguaje de primer orden de la aritmética, lo que significa que puede expresarse usando solo cuantificadores sobre números naturales ("para todos los números naturales x" o "existe un número natural x"), sin cuantificar sobre conjuntos de números naturales. A primera vista, puede parecer muy restrictivo prohibir la cuantificación sobre conjuntos de enteros; sin embargo, los conjuntos finitos de enteros se pueden "codificar" usando un solo entero, por lo que está bien cuantificar sobre conjuntos finitos de enteros.

PNP

Pero espere, puede decir, ¿qué pasa con las declaraciones aritméticas cuya prueba requiere algo como el lema de Koenig o el teorema del árbol de Kruskal? ¿No requieren estos una forma débil del axioma de elección? La respuesta es que depende exactamente de cómo declare el resultado en cuestión. Por ejemplo, si establece el teorema menor del gráfico en la forma, "dado cualquier conjunto infinito de gráficos sin etiquetar, deben existir dos de ellos de modo que uno sea menor que el otro", entonces se necesita cierta cantidad de opciones para avanzar su conjunto infinito de datos, seleccionando vértices, subgráficos, etc. [EDITAR: cometí un error aquí. Como explica Emil Jeřábek, el teorema menor del gráfico, o al menos el enunciado más natural del mismo en ausencia de CA, es demostrable en ZF. Pero modulo este error, lo que digo a continuación sigue siendo esencialmente correcto. ] Sin embargo, si en cambio escribe una codificación particular por números naturales de la relación menor en gráficos finitos etiquetados, y formula el teorema menor del gráfico como una declaración sobre este orden parcial en particular, entonces la declaración se vuelve aritmética y no requiere AC en la prueba.

La mayoría de la gente siente que la "esencia combinatoria" del teorema menor del gráfico ya está capturada por la versión que corrige una codificación particular, y que la necesidad de invocar AC para etiquetar todo, en caso de que se presente el conjunto general, La versión teórica del problema es una especie de artefacto irrelevante de una decisión de utilizar la teoría de conjuntos en lugar de la aritmética como fundamento lógico. Si siente lo mismo, entonces el teorema menor del gráfico no requiere AC. (Vea también esta publicación de Ali Enayat en la lista de correo de Fundamentos de las Matemáticas, escrita en respuesta a una pregunta similar que una vez tuve).

El ejemplo del número cromático del plano es igualmente una cuestión de interpretación. Hay varias preguntas que puede hacer que resultan equivalentes si asume CA, pero que son preguntas distintas si no asume CA. Desde el punto de vista de TCS, el corazón combinatorio de la pregunta es la colorabilidad de los subgrafos finitos del plano, y el hecho de que usted puede (si lo desea) usar un argumento de compacidad (aquí es donde entra AC) para concluir algo El número cromático de todo el plano es divertido, pero de interés algo tangencial. Así que no creo que este sea un muy buen ejemplo.

Creo que, en última instancia, es posible que tenga más suerte al preguntar si hay preguntas de TCS que requieren grandes axiomas cardinales para su resolución (en lugar de AC). El trabajo de Harvey Friedman ha demostrado que ciertas declaraciones finitarias en la teoría de grafos pueden requerir grandes axiomas cardinales (o al menos la consistencia 1 de tales axiomas). Los ejemplos de Friedman hasta ahora son ligeramente artificiales, pero no me sorprendería ver ejemplos similares surgiendo "naturalmente" en TCS en nuestras vidas.

Timothy Chow
fuente
8
Probar la normalización para el cálculo lambda mecanografiado con polimorfismo requiere al menos aritmética de segundo orden, y mostrar lo mismo para las teorías de tipo más generosas puede requerir grandes axiomas cardinales, aunque bastante modestos. IIRC, la prueba de normalización de Coq necesita muchos inaccesibles, ya que puede usarla para codificar argumentos de universo de estilo Grothendieck.
Neel Krishnaswami
3
@Neel: Buen punto, aunque IMO estos ejemplos "engañan" porque es bastante obvio que podría necesitar axiomas lógicos fuertes para demostrar la consistencia de un sistema lógico.
Timothy Chow
44
Me gusta esta respuesta porque explica por qué el uso del axioma de elección en TCS parece extremadamente raro.
Tsuyoshi Ito
11
Π31Π31ZFCZF
1
Esta respuesta aparece en el blog de la comunidad.
Aaron Sterling
39

Según tengo entendido, la prueba conocida del teorema de Robertson-Seymour utiliza el Axioma de elección (a través del teorema del árbol de Kruskal). Esto es considerablemente interesante desde el punto de vista de TCS, ya que el teorema de Robertson-Seymour implica que las pruebas de membresía en cualquier familia de gráficos cerrados menores se pueden hacer en tiempo polinómico. En otras palabras, el Axioma de Elección puede usarse indirectamente para demostrar que existen algoritmos de tiempo polinomiales para ciertos problemas, sin construir realmente esos algoritmos.

Sin embargo, esto podría no ser exactamente lo que está buscando, ya que no está claro si realmente se requiere CA aquí.

Janne H. Korhonen
fuente
Este es un buen comienzo, ya que no se sabe cómo probar el teorema de lo contrario.
Ryan Williams
77
Como se menciona en la página de Wikipedia, el artículo de Friedman, Robertson y Seymour sobre la metamatemática del teorema del gráfico menor muestra que el teorema del gráfico menor implica (una forma de) el teorema del árbol de Kruskal sobre la teoría básica RCA_0, por lo que esto establece que Kruskal El teorema del árbol se requiere para el teorema menor del gráfico en un sentido fuerte. Sin embargo, si esto significa que se requiere el axioma de elección para el teorema menor del gráfico es una pregunta un poco difícil. Depende de manera sutil de cómo eliges establecer el teorema menor del gráfico. Vea mi respuesta para más detalles.
Timothy Chow
77
Emil Jeřábek ha mostrado en MathOverflow cómo probar el teorema de Robertson-Seymour sin el axioma de elección. Esto me sorprendió porque también tenía la impresión de que el Robertson-Seymour para gráficos sin etiquetar requería AC, pero eso era evidentemente una impresión errónea.
Timothy Chow
Entonces, ¿la respuesta aceptada es realmente falsa?
Andrej Bauer
@AndrejBauer: Si te refieres a mi respuesta, tienes razón en que lo que dije sobre Robertson-Seymour está mal. Traté de editar mi respuesta en este momento pero no pude. Tal vez no tengo suficiente reputación para editar una publicación tan antigua.
Timothy Chow el
21

Esto se relaciona con la respuesta dada por Janne Korhonen.

Hubo una corriente de resultados en los años 80 y 90 que intentaron caracterizar los sistemas de axiomas (en otras palabras, la teoría aritmética) necesarios para probar extensiones del Teorema del árbol de Kruskal (KTT; el KTT original es de 1960). En particular, Harvey Friedman demostró varios resultados siguiendo esta línea (ver SG Simpson. No demostrabilidad de ciertas propiedades combinatorias de árboles finitos . En LA Harrington et al., Editor, Harvey Friedman Research on Foundations of Mathematics. Elsevier, North-Holland, 1985) . Estos resultados mostraron que (ciertas extensiones de) KTT deben usar axiomas de comprensión "fuertes" (es decir, axiomas que dicen que existen ciertos conjuntos de alta complejidad lógica). No sé exactamente acerca de la posibilidad de probar las extensiones de KTT en ZF (sin el axioma de elección).

Paralelamente a este flujo de resultados, hubo un intento de conectarlo a TCS ("Teoría B") a través de sistemas de reescritura . La idea es construir sistemas de reescritura (piense en ello como una especie de programación funcional, o programas de cálculo lambda) para los cuales su terminación depende de ciertas (extensiones) de KTT (la conexión original entre KTT y la terminación de los sistemas de reescritura fue probada por N Dershowitz (1982)). Esto implica que para mostrar que ciertos programas terminan, uno necesita axiomas fuertes (ya que las extensiones de KTT necesitan tales axiomas). Para este tipo de resultados, ver, por ejemplo, A. Weiermann, Límites de complejidad para algunas formas finitas del teorema de Kruskal , Journal of Symbolic Computation 18 (1994), 463-488.

Iddo Tzameret
fuente
16

R2

En Shelah y Soifer, "Axioma de elección y número cromático del plano" , se muestra que si todas las subgrafías finitas del plano son cuatro cromáticas, entonces

  • Si asume el axioma de elección, entonces el plano es cuatro cromático.
  • Si asume el principio de las elecciones dependientes y que todos los conjuntos son medibles en Lebesgue, entonces el plano es cinco, seis o siete cromáticos.
Derrick Stolee
fuente
¿No es esto más orientado a las matemáticas que a TCS?
MS Dousti
Es por eso que dije "tangencialmente" relacionado. Los problemas de coloración están orientados a TCS, solo que no son específicos.
Derrick Stolee
44
α
Excelente. Validación.
Derrick Stolee
5

Parte del trabajo de Olivier Finkel parece estar relacionado con la pregunta, aunque no necesariamente de manera explícita sobre el Axioma de Elección en sí mismo, y en línea con la respuesta de Timothy Chow. Por ejemplo, citando el resumen de teoremas de incompletitud, grandes cardenales y autómatas sobre palabras finitas , TAMC 2017 ,

Tn:=ZFC+``There exist (at least) n inaccessible cardinals''n0
Sylvain
fuente
3

[Esta no es una respuesta directa a su pregunta, pero puede ser sugerente y / o informativa para algunas personas.]

La encuesta P vs. NP de William Gasarch ofrece algunas estadísticas sobre "cómo se resolverá P vs. NP":

  1. 61 pensaban P ≠ NP.
  2. 9 pensaban P = NP.
  3. 4 pensaron que es independiente . Si bien no se mencionó ningún sistema de axiomas en particular, supongo que piensan que es independiente de ZFC .
  4. 3 acaba de afirmar que NO es independiente de la aritmética recursiva primitiva.
  5. Dije que dependería del modelo.
  6. 22 no ofrecieron opinión.

Wikipedia tiene una interesante toma de independencia:

... Estas barreras también han llevado a algunos informáticos a sugerir que el problema P versus NP puede ser independiente de los sistemas de axiomas estándar como ZFC (no se puede probar ni refutar dentro de ellos). La interpretación de un resultado de independencia podría ser que no existe un algoritmo de tiempo polinomial para ningún problema de NP completo, y tal prueba no se puede construir en (por ejemplo) ZFC, o que pueden existir algoritmos de tiempo polinomial para problemas de NP completo, pero es imposible probar en ZFC que tales algoritmos son correctos [ 1] Sin embargo, si se puede demostrar, utilizando técnicas del tipo que actualmente se sabe que son aplicables, que el problema no puede decidirse incluso con suposiciones mucho más débiles que extienden los axiomas de Peano (PA) para la aritmética de enteros, entonces necesariamente existiría casi- algoritmos de tiempo polinómico para cada problema en NP [ 2 ]. Por lo tanto, si uno cree (como lo hacen la mayoría de los teóricos de la complejidad) que no todos los problemas en NP tienen algoritmos eficientes, se deduciría que las pruebas de independencia usando esas técnicas no pueden ser posibles. Además, este resultado implica que probar la independencia de PA o ZFC utilizando técnicas conocidas actualmente no es más fácil que demostrar la existencia de algoritmos eficientes para todos los problemas en NP.

MS Dousti
fuente
55
Otro hecho interesante (también de Wikipedia) es que, la técnica general principal (¿única?) Para probar la independencia en ZFC, forzar, no puede probar que P =? NP es independiente de ZFC. Este es un corolario del teorema de la absolutidad de Shoenfield.
Servicio de Travis el
Tenga en cuenta que Bill está tomando otra encuesta, que está abierta por otro mes más o menos: blog.computationalcomplexity.org/2011/06/…
Charles
@ Charles: Gracias por la actualización. Estoy realmente ansioso por conocer el consenso más reciente de la comunidad.
MS Dousti
2

ZF

Gχ(H)HGG

ZF

Stella Biderman
fuente
Buen ejemplo Creo que Timothy Chow se dirigió a este tipo de ejemplo en el párrafo sobre el número cromático del avión.
Sasho Nikolov
@SashoNikolov La capacidad de coloración de los gráficos es, en mi opinión, claramente un problema de TCS incluso cuando los gráficos son infinitos. El problema de Hadwiger-Nelson es mucho menos evidente en el ámbito de TCS, como señalaron los comentaristas y el OP de esa respuesta estuvo de acuerdo. Por el contrario, no creo que haya nadie que vea este teorema y diga "eso no es realmente un problema de CS"
Stella Biderman
No veo la distinción en absoluto: Hadwiger-Nelson también se trata de colorear un gráfico geométrico infinito. En cualquier caso, en realidad me gustan y votaron a favor de ambos ejemplos y creo que no tiene sentido tratar de establecer una distinción demasiado fina entre TCS y otras áreas de las matemáticas.
Sasho Nikolov