¿Consecuencias computacionales del teorema de punto fijo de cambio superior (no demostrable) de Friedman?

Harvey Friedman demostró que hay un claro resultado de punto fijo que no se puede probar en ZFC (la teoría de conjuntos Zermelo-Frankel habitual con el Axioma de Elección). Muchas lógicas modernas se basan en operadores de punto fijo, así que me preguntaba: ¿hay alguna consecuencia conocida del teorema del punto fijo de cambio superior para la informática teórica?

Teorema de punto fijo de cambio superior no demostrable
Para todos , algo de A = cubo ( A , 0 ) ∖ R [ A ] nos contiene ( A ) .$R \in \text{SDOI}(Q^k,Q^k)$$A = \text{cube}(A,0) \setminus R[A]$$\text{us}(A)$

El teorema de USFP parece ser una declaración , por lo que podría estar "lo suficientemente cerca" de la computabilidad (como verificar el no isomorfismo de las estructuras automáticas) para impactar la ciencia de la computación teórica.$\Pi^1_1$

Para completar, aquí están las definiciones de la charla MIT de Friedman de noviembre de 2009 (véase también el borrador del libro sobre "Teoría de la relación booleana" ).

es el conjunto de números racionales. x , y ∈ Q k sonequivalentes de ordensi siempre que 1 ≤ i , j ≤ k, entonces x i < x j ⇔ y i < y j . Cuando x ∈ Q k , eldesplazamiento superiorde x , denotado us ( x ) , se obtiene sumando 1 a cada coordenada no negativa de x . Una relación$Q$$x, y \in Q^k$$1 \le i,j \le k$$x_i \lt x_j \Leftrightarrow y_i \lt y_j$$x \in Q^k$$x$$\text{us}(x)$$x$ esorden invariantesi para cada ordeninvarianteequivalente x , y ∈ Q k se cumple que x ∈ A ⇔ y ∈ A . Una relación R ⊆ Q k × Q k es invariante de orden si R es invariante de orden como un subconjunto de Q 2 k , y esestrictamente dominantesi para todo x , y ∈ Q k siempre que R $A \subseteq Q^k$ $x,y \in Q^k$$x \in A \Leftrightarrow y \in A$$R \subseteq Q^k \times Q^k$$R$$Q^{2k}$$x,y \in Q^k$$R(x,y)$$\max(x) \lt \max(y)$$A$$Q^k$$R[A]$$\{ y | \exists x \in A R(x,y)\}$$A$$\text{us}(A) = \{\text{us}(x) | x \in A\}$$\text{cube}(A,0)$$B^k$$0 \in B$$A$$B^k$$\text{SDOI}(Q^k,Q^k)$$R \subseteq Q^k \times Q^k$

Editar: como señala Dömötör Pálvölgyi en los comentarios, tomar y como el orden habitual de los racionales parece dar un contraejemplo. Primero, el conjunto no puede estar vacío, ya que también está vacío y tendría que contener 0 por la condición del cubo, una contradicción. Si el conjunto no vacío tiene un infimum, entonces no puede contener ningún racional mayor que este, por lo que debe ser un singleton, lo que contradice la condición de desplazamiento superior. Si, por otro lado, no tiene infimum, entonces entonces debe estar vacío, una contradicción. $k=1$$R$$A$$R[A]$$A$$A$$A$$R[A] = Q$$A$¿Algún comentario sobre si existen problemas ocultos de definición no obvios, como quizás un modelo implícito no estándar de los racionales?

Edición adicional: el argumento anterior es más o menos correcto, pero está mal en la aplicación del cambio superior. Este operador solo se aplica a coordenadas no negativas , por lo que establecer como cualquier conjunto único negativo produce un punto fijo, como se desee. En otras palabras, si entonces es una solución, y no hay otras soluciones.$A$$m < 0$$A = \{m\}$

No conozco ninguna consecuencia de este teorema en particular, pero las pruebas de normalización de cálculos lambda como el cálculo de las construcciones inductivas se basan en grandes axiomas cardinales, aunque el conjunto de términos lambda es tan contable como podría desear.

Creo que la mejor manera de comprender la importancia computacional de los axiomas de la teoría de conjuntos que afirman la existencia de grandes cardinales es pensar en la teoría de conjuntos como una forma de formular la teoría de los gráficos. Es decir, un modelo de un conjunto es una colección de elementos equipados con una relación binaria utilizada para interpretar la pertenencia. Luego, los axiomas de la teoría de conjuntos le indican las propiedades de la relación de pertenencia, incluida la forma en que puede formar nuevos conjuntos a partir de los antiguos. En particular, el axioma de la fundación significa que la relación de membresía está bien fundada (es decir, no tiene cadenas descendentes infinitas). Esta fundamentación a su vez significa que si puede alinear los estados de ejecución de un programa con la pertenencia transitiva de los elementos de un conjunto, entonces tiene una prueba de terminación.

Entonces, una afirmación de que existe un conjunto "grande" tiene una recompensa computacional como un reclamo de que cierta clase de bucles en un lenguaje de programación recursivo general termina. Esta interpretación funciona de manera uniforme, desde el antiguo axioma simple del infinito (que justifica la iteración de números naturales) hasta los axiomas cardinales grandes.

¿Son ciertos estos axiomas ? Bueno, si el axioma es falso, puede encontrar un programa en una de estas clases que no termina. Pero si es verdad, nunca estaremos seguros, gracias al teorema de Halting. Todo, desde la inducción de números naturales en adelante, es una cuestión de inducción científica , que siempre puede ser falsificada por experimentos: ¡Edward Nelson ha esperado demostrar que la exponenciación es una función parcial!