¿Existen resultados de indecidibilidad que no se saben que tengan una demostración por argumento diagonal?

Question

¿Existe algún problema que se sabe que es indecidible (en el sentido algorítmico), pero para el cual las únicas pruebas conocidas de indecidibilidad no utilizan alguna forma del argumento diagonal de Cantor de manera esencial?

Debo admitir libremente que esta es una pregunta algo mal formulada, por varias razones:

1. Uno podría tomar una prueba que no use diagonalización e insertar una invocación gratuita del argumento diagonal para evitar una respuesta positiva a esta pregunta por una cuestión técnica. (Por lo tanto, el calificador "esencial" en la pregunta anterior tiene que hacer mucho trabajo pesado.)
2. Como señaló Timothy Chow en esta respuesta anterior de MO, no hay una noción bien definida de lo que significa "usar diagonalización".
3. Muchos resultados de indecidibilidad no mencionan la diagonalización en el nivel superior de su prueba, sino que se basan en reducciones a otros resultados de indecidibilidad, como la indecidibilidad del problema de detención, que generalmente se demuestran mediante diagonalización.

De todos modos, espero que el espíritu de la pregunta siga siendo claro, a pesar de su falta de precisión.

Dos observaciones:

1. La indecidibilidad del problema de detención en sí misma ciertamente tiene pruebas que posiblemente no invoquen la diagonalización (algunas de ellas se enumeran aquí). Pero esto no sería una respuesta positiva a mi pregunta, porque la indecidibilidad del problema de detención también tiene la prueba de libro de texto que usa la diagonalización.
2. Ciertamente hay resultados de indecidibilidad que no se prueban simplemente mediante reducción al problema de detención; consulte las respuestas a esta pregunta anterior de MO para ver varios ejemplos. Es posible que uno de los resultados mencionados allí sea ya una respuesta candidata a mi pregunta, aunque no pude identificar fácilmente dicho candidato.

Answer 1

Esto no es realmente una respuesta, sino una posible forma de formalizar tu pregunta. En mi opinión, la "esencia" de una prueba de estilo diagonal de indecidibilidad es que señala explícitamente la entrada en la que cada máquina potencial falla al resolver el problema dado: si $\mathcal{L}$ es nuestro lenguaje/función difícil, la prueba de indecidibilidad proporciona un procedimiento constructivo que toma el código de cualquier máquina supuesta $M$ que resuelve $\mathcal{L}$, y muestra un (lista de) entrada(s) donde debe ocurrir un error. Lo siguiente es una forma directa de formalizar esto, y creo que captura una noción bastante amplia de pruebas de indecidibilidad de estilo diagonal:

Definición. Sea $\mathcal{L} \subseteq \{0,1\}^*$ un lenguaje. Un "certificador" de la indecidibilidad de $\mathcal{L}$ es una función computable total $\mathcal{C}$ que tiene el siguiente comportamiento. En la entrada de una descripción de máquina $M$, $\mathcal{C}(M)$ imprime una lista de entradas $x_1,\ldots,x_k \in \{0,1\}^*$ tales que para algún $i \leq k$, $M(x_i) \neq \mathcal{L}(x_i)$ (es decir, o bien $M$ hace un bucle infinito en $x_i$ o bien $M$ se detiene con el valor incorrecto en $x_i$). Decimos que $\mathcal{L}$ es "certificablemente indecidible" si tiene un certificador.

Básicamente el mismo concepto ha sido estudiado en teoría de la complejidad bajo el nombre de "refutador," por ejemplo, aquí.

Es fácil ver que el problema de la detención es certificablemente indecidible usando el argumento clásico; a partir de la descripción del supuesto solucionador del problema de detención $M$ podemos construir la máquina diagonal $D_M$ usando $M$ como su prueba de detención; luego $\mathcal{C}(M)$ puede producir $\langle D_M,D_M\rangle$. En el caso de la complejidad de Kolmogorov, dada $M$ podemos elegir $n$ suficientemente grande que la longitud de la descripción de $M$ y producir todas las cadenas de longitud $n$; un argumento básicamente idéntico funciona para Busy Beaver.

También es fácil ver que los lenguajes certificablemente indecidibles son cerrados hacia arriba bajo reducciones de tabla de verdad computables; si $\mathcal{L} \leq_{tt} \mathcal{L}'$ podemos transformar el certificador de $\mathcal{L}$ en uno para $\mathcal{L}'$ enumerando las consultas hechas cuando componemos el certificador con la reducción. Esto también se cumple para una noción más fuerte de reducción donde las consultas a un oráculo se pueden hacer en secuencia, pero el número total de consultas al oráculo está limitado por encima en la longitud de la entrada por una función computable total; no estoy seguro de una reducción Turing general.

En esta formulación, tu pregunta se puede formalizar como: ¿es cada lenguaje indecidible certificablemente indecidible? Si hay un contraejemplo, debe ser intermedio entre $0$ y $0'$, al menos con respecto a las nociones restringidas de reducibilidad mencionadas anteriormente. No tengo idea de si alguno de los lenguajes intermedios conocidos son un buen candidato para esto.

Answer 2

EDICIÓN: Después de reflexionar, esta respuesta es bastante incorrecta. Hay un punto aquí, pero está formulado de manera tan deficiente que creo que debería ser ignorado. No estaba seguro de cuál es la mejor práctica para una respuesta incorrecta, así que dejaré un comentario con las correcciones.

Perdona tanto la respuesta tardía como el comentario potencialmente ingenuo, pero tal vez ayude desglosar el teorema de Lawvere y preguntar si se puede construir una prueba de indecidibilidad no diagonal.

Una prueba de indecidibilidad tiene la anatomía aproximada de que queremos encontrar algún epimorfismo $g: A \to Y^S = g: A \to S \to Y$ tal que la imagen de $g$ sea monomórfica. En el caso habitual de que $A = S$ sea un conjunto y $Y$ sea un conjunto finito, $g$ selecciona algún $h: A \to Y$ que asigna algún $y \in Y$ a cada $a \in A$, o en otras palabras, $g$ encuentra, para cada $A$, algún $h$ que decide los $a$s. Luego encontramos que asumiendo que existe dicho epimorfismo, obtenemos una contradicción, por lo tanto $A$ no es generalmente decidible.

Las pruebas de indecidibilidad son, creo de todos modos, quintesencialmente no constructivas, por lo que tenemos que asumir la decidibilidad (es decir, que existe un $g$) y mostrar que conduce a una contradicción (explícitamente o no) para obtener una prueba de indecidibilidad. Asumir que existe un epimorfismo $g$ es un elemento estrictamente necesario.

Luego, solo desenrrollando, podemos mostrar que $g$ es isomorfo a $f: A \times S \to Y$. Luego, el morfismo diagonal $\Delta: A \to A \times S$, que forma una pareja de identidad $\Delta(a) = (a, a)$ en el caso habitual, no agrega mucho, ya que $f \circ \Delta$ es isomorfo a $g \circ id_A = g$ (más generalmente, $f \circ \Delta$ es isomorfo a algún $g \circ i$ donde $i: A \to A$ es un isomorfismo). La respuesta de Joel anterior sugirió que la aplicación del morfismo diagonal podría considerarse como un paso fundamental para distinguir una diagonalización, pero para mí parece ser realmente trivial. En el mejor de los casos, las pruebas no diagonales vistas de esta manera aplican un isomorfismo $A \to A$ antes de hacer su trabajo.

En esta etapa, creo que la mayoría de una prueba de diagonalización es necesaria, incluida, en efecto, la parte diagonal, para mostrar la indecidibilidad. Al menos, si encontramos una prueba que no parece involucrar diagonalización, podemos estar bastante seguros de que no debería ser demasiado difícil transformarla en un argumento que use un $\Delta$.

El paso final en la diagonalización es elegir $\alpha: Y \to Y$ sin puntos fijos. Dado que podemos elegir tal $\alpha$, al aplicar $\alpha \circ f \circ \Delta: A \to Y$, mostramos que $f \circ \Delta$ no es único hasta isomorfismo $A \to A$, y por lo tanto $g$ no puede ser un epimorfismo. Si estamos buscando alternativas a la diagonalización, el lugar podría estar aquí. Podría haber un enfoque no trivialmente diferente para mostrar que $g$ no puede ser un epimorfismo. Aunque, para resultados de indecidibilidad, me resulta difícil imaginar cómo se prueba que no se puede encontrar un $h$ que decida arbitrariamente $a$ que no sea eligiendo $\alpha \circ h$ que haga algún tipo de asignación de decisión inversa.

Para resumir una respuesta larga, si no he cometido algún error básico, creo que la respuesta a la pregunta puede ser "no, y además, no puede haberlo".

Correcciones:

1. Una instancia de una prueba de indecidibilidad supone la existencia de un morfismo único $g: A \to Y$. Asumir que $g: A \to S \to Y$ es casi todo el trabajo duro en una prueba de diagonalización/Lawvere, y no es estrictamente necesario para demostrar la indecidibilidad.
2. Para pasar de la indecidibilidad a Lawvere, permitimos que $g = h \circ k \circ id_A: A \to A \to S \to Y \sim A \to A \times S \to Y$, donde $k$ es un isomorfismo. Para instancias donde $S = A$, $k$ es trivial como sugiere lo anterior (y podría igualmente ser la identidad), pero eso no siempre es así.
3. Para que $g$ sea único, $g \equiv \alpha \circ h \circ k \circ id_A \sim \alpha \circ f \circ \Delta$ para cualquier elección de $\alpha$, pero, dado que siempre podemos elegir $\alpha: Y \to Y$ sin puntos fijos (ya que $Y$ es no degenerado), esto no puede ser.

Así que aquí está el meollo. $k$ no siempre podría ser trivial (aunque estos son casos en los que queremos pasar a $S$ porque es más fácil hacer afirmaciones sobre $S \to Y$ que sobre $A \to Y$), pero si tenemos una prueba de que no existe un morfismo único $g$, entonces siempre podemos transformar esto en una prueba sobre $g \circ id_A \circ id_A \sim f \circ \Delta$. Sin embargo, puedo imaginar casos donde hacerlo es innecesario y este movimiento parece superfluo. Aunque no me parece que sea siempre $g = h$ (por ejemplo, el problema de detención), así que tal vez sea solo una ilusión óptica.

Todavía no estoy seguro de si lo he entendido correctamente, pero creo que al menos vale la pena admitir el error.