É possível testar duas consultas SO-Horn para obter equivalência?

Segue-se do teorema de Rice que você não pode determinar se duas máquinas de Turing decidem ou não o mesmo idioma. Minha pergunta é: Isso também se aplica a configurações descritivas de complexidade, principalmente quando se trata de testar um par de consultas SO-Horn para ver se elas descrevem o mesmo idioma? Não conheço nenhuma versão descritiva da complexidade do teorema de Rice e pude imaginar que talvez não seja tão difícil testar duas fórmulas de segunda ordem quanto à equivalência.

Primeiro, observe que a igualdade de duas TMs é mais difícil que o problema de parada (é -complete), ou seja, você não pode computá-la nem com um oráculo para o problema de parada. Portanto, nem é ce (ou seja, , akare). O teorema de Rice implica que o conjunto não é ce, não implica o resultado mais forte.$\Pi^0_2$$\Sigma^0_1$

Existe uma versão teórica da complexidade do teorema de Rice (de D. Kozen), mas que fornece um resultado mais fraco, o que é esperado, podemos verificar propriedades não triviais se soubermos que a máquina pára, por exemplo, podemos verificar se a máquina aceita quando executado em uma fita vazia. Intuitivamente, o resultado diz (mais ou menos) que a única maneira de verificar propriedades não triviais da linguagem das TMs é simular as máquinas (se bem me lembro).

A complexidade descritiva não muda as coisas, então acho que você pode ignorá-la e substituí-la pelas TMs por relógios polinomiais (eles podem ser convertidos em caracterização descritiva da complexidade e a caracterização descritiva da complexidade pode ser convertida em caracterização usando TMs).

Acho que a questão de decidir a igualdade de funções ainda mais simples é co-ce-completa (ou seja, -complete). Não podemos verificar se dois multinomiais são equivalentes aos números naturais (já que o complemento é ce-completo pelo teorema MRDP), e isso implica que não podemos verificar a igualdade de duas consultas SO-Horn.$\Pi_1$