¿Se pueden probar dos consultas SO-Horn para determinar la equivalencia?

Del teorema de Rice se deduce que no se puede determinar si dos máquinas de Turing deciden o no el mismo idioma. Mi pregunta es: ¿Esto también se aplica en configuraciones de complejidad descriptiva, particularmente cuando se trata de probar un par de consultas SO-Horn para ver si describen el mismo idioma? No conozco ninguna versión de complejidad descriptiva del teorema de Rice, y posiblemente podría ver que podría no ser tan difícil probar la equivalencia de dos fórmulas de segundo orden.

Primero, tenga en cuenta que la igualdad de dos TM es más difícil que el problema de detención (es -completo), es decir, no puede calcularlo incluso con un oráculo para el problema de detención. Por lo tanto, ni siquiera es ce (es decir, Σ 0 1 , akare). El teorema de Rice implica que el conjunto no es ce, no implica el resultado más fuerte.$\Pi^0_2$$\Sigma^0_1$

Existe una versión teórica de la complejidad del teorema de Rice (por D. Kozen), pero que da un resultado más débil, que es de esperar, podemos verificar propiedades no triviales si sabemos que la máquina se detiene, por ejemplo, podemos verificar si la máquina acepta cuando se ejecuta en una cinta vacía. Intuitivamente, el resultado dice (más o menos) que la única forma de verificar las propiedades no triviales del lenguaje de TM es simular las máquinas (si no recuerdo mal).

La complejidad descriptiva no cambia las cosas, por lo que creo que puede ignorarlo y simplemente reemplazarlo con los TM con relojes polinomiales (se pueden convertir en caracterización de complejidad descriptiva y la caracterización de complejidad descriptiva se puede convertir en caracterización usando TM).

$\Pi_1$