Resultados en CS teórico independiente de ZFC

37

Voy a hacer una pregunta bastante vaga, ya que la frontera entre la informática teórica y las matemáticas no siempre es fácil de distinguir.

PREGUNTA: ¿Conoce algún resultado interesante en CS que sea independiente de ZFC (es decir, la teoría de conjuntos estándar), o que se demostró originalmente en ZFC (+ algún otro axioma) y solo se demostró más tarde en alorne ZFC?

Lo pregunto porque estoy cerca de terminar mi tesis doctoral, y mi resultado principal (la determinación de una clase de juegos que se utilizan para dar "semántica de juego" a un cálculo modal probabilístico) está actualmente demostrada en ZFC se extendió con otros Axiomas (es decir, la negación de la hipótesis del Continuo ¬ C H y el Axioma de Martin M A ).μ¬CHMA

Por lo tanto, la configuración es claramente informática (el cálculo modal es una lógica temporal, y lo estoy extendiendo para que funcione con sistemas probabilísticos).μ

Quisiera citar en mi tesis otros ejemplos (si conoce alguno) de este tipo.

Gracias de antemano,

adiós

Matteo

IamMeeoh
fuente
99
Estas preguntas anteriores pueden ser útiles: cstheory.stackexchange.com/questions/4816/… cstheory.stackexchange.com/questions/1923/…
Mark Reitblatt
99
Iba a responder que Matteo Mio y Alex Simpson usaron el Axioma de Martin para probar resultados muy interesantes ...
Andrej Bauer
77
¡Este puede ser el mejor ejemplo que he visto de una pregunta cuya mejor respuesta está contenida en la pregunta misma! No estaba al tanto de su resultado muy interesante.
Timothy Chow

Respuestas:

19

Si bien no conozco ninguno de estos resultados, aparte del suyo, creo que podría ampliar un poco el alcance y preguntar: qué resultados en TCS se han demostrado utilizando (cualquier tipo de) axiomas no estándar. Por no estándar aquí me refiero a algo más que la lógica clásica con ZF (o ZFC).

Un hermoso ejemplo del tipo de trabajo que tengo en mente son los resultados de Alex Simpson sobre las propiedades de los lenguajes de programación que utilizan la teoría de dominio sintético. Utiliza la teoría de conjuntos intuicionista con axiomas que contradicen la lógica clásica.

Además, Alex y yo usamos axiomas intuicionistas con principios de continuidad anticlásicos para mostrar resultados sobre la computabilidad de Banach-Mazur.

Sin embargo, ninguno de los ejemplos mencionados tiene un estado "abierto", como sus pruebas, porque sabemos que los axiomas no estándar que utilizamos pueden entenderse simplemente como trabajando dentro de un modelo de matemática intuicionista, donde se puede demostrar que el modelo existe en ZFC Por lo tanto, la configuración no estándar es realmente una forma de hacer las cosas de manera más elegante, y en principio podrían hacerse en ZFC directo (aunque me temo pensar cómo sería exactamente eso).

Andrej Bauer
fuente
¡Gracias! Le preguntaré a Alex más detalles sobre esto cuando esté escribiendo la introducción.
IamMeeoh
13

Depende de su definición de "informática". Tome el siguiente ejemplo: ¿cuenta?

A la codificación de los números enteros es un código binario de forma única decodificable de . Si la longitud de las palabras de código no disminuye, llamamos al código monótono . Un código C 1 es mejor que un código C 2 si | C 1 ( n ) | - | C 2 ( n ) | - . En otras palabras, para cada L , desde algún punto en las palabras de código de C 1 son al menos L bits más cortos.NC1C2|C1(n)||C2(n)|LC1L

Un conjunto de códigos se llama cofinal si para cada código de C hay un código D S , que es mejor que C . Está bien ordenado si está bien ordenado con respecto a "mejor". Una escala es un conjunto de códigos cofinales bien ordenados.SCDSC

Aquí hay dos propiedades que son independientes de ZFC:

  1. Existe una escala de códigos.
  2. Existe una escala de códigos monótonos (es decir, un conjunto bien ordenado de códigos monótonos que es cofinal en el conjunto de todos los códigos monótonos).
Yuval Filmus
fuente
Hola Yuval, gracias por la respuesta. No estoy seguro de que su ejemplo se ajuste a mi definición "Informática". Seguramente hablar de "códigos" no es suficiente para clasificarlo como CS. Lo que hace que un artículo sea "un documento de CS" es lo siguiente: ¿Apareció en alguna conferencia / diario de CS, o se usó para probar algún resultado en una conferencia / diario de CS? por CS paper soy bastante flexible, pero los temas podrían ser "teoría de la información, complejidad, lógica de programas / sistemas, teoría de la recursión" etc. De todos modos, puede citar la fuente del ejemplo y / o documentos que hacen uso de "existe una escala de códigos "? ¡Gracias! Bye
IamMeeoh
1
Los artículos sobre los códigos de los enteros aparecen en revistas de ingeniería eléctrica, como las transacciones IEEE sobre teoría de la información. Eso golpea una de tus palabras clave.
Yuval Filmus
1
No creo que haya ningún documento que use estos resultados. Además, creo firmemente que un resultado independiente de ZFC no tiene ningún uso en complejidad, por lo que, en cierto sentido, su pregunta es acerca de ampliar los límites de lo que se considera informática.
Yuval Filmus
1
Hola Yuval, antes que nada déjame agradecerte nuevamente por las respuestas. Sin embargo, no estoy de acuerdo con tu fuerte posición. Por ejemplo, el teorema de Robertson-Seymour (que parece requerir elección) tiene importantes consecuencias en la complejidad. Por lo tanto, está claro que la elección es útil (quizás un poco sorprendente) en la teoría de la complejidad. Ahora, trabajar con extensiones consistentes de ZFC obviamente simplifica la tarea de probar, digamos la complejidad, resultados, incluso si estos resultados pueden ser demostrables en ZFC pero nadie sabe cómo, todavía.
IamMeeoh
1
Además, no veo por qué no debería haber resultados concretos en la complejidad independiente de ZFC, de la misma manera que el teorema de Robertson-Seymour es (quizás) independiente de ZF.
IamMeeoh
9

DbDcbTccD

La declaración de la determinación del grado de Turing :

Cada conjunto de grados de Turing contiene un cono o es disjunto de algún cono

es una consecuencia del axioma de determinación (AD), que es independiente de ZF e incompatible con ZFC. La declaración más débil

Cada conjunto de reales de Borel que se cierra bajo la equivalencia de Turing contiene un cono o está separado de un cono

es una consecuencia del teorema de Martin sobre la determinación de Borel, que es demostrable en ZFC. Ambas declaraciones fueron estudiadas antes de que se probara el resultado de Martin sobre la determinación de Borel, en ese momento solo se sabía que ambas son demostrables en ZF + AD.

SbcSbTcSS

Carl Mummert
fuente
0

Muchas matemáticas constructivas. Vea el trabajo de Per Martin-Löf sobre la teoría de conjuntos constructivos, utilizada como base para lenguajes de programación de tipo dependiente.

Robar
fuente
66
IIRC, la teoría de tipo Martin-Lof tiene la misma fuerza de consistencia que la teoría de conjuntos de Kripke-Platek, que es mucho más débil que ZFC. Además, MLTT no tiene ningún principio explícitamente anticlásico, como los axiomas de continuidad que Andrej mencionó.
Neel Krishnaswami
@Neel Nunca dije nada sobre la consistencia o fortaleza de MLTT. Sin embargo, considero que algunos resultados en matemáticas constructivas son relevantes para la pregunta, pidiendo "resultados interesantes en CS que sean ... independientes de ZFC".
Rob
55
Supongo que "independiente" aquí se entiende en el sentido formal.
Mark Reitblatt