# Is testing two SO-Horn queries for equivalence decidable?

It follows from Rice's theorem that you cannot determine whether or not two Turing machines decide the same language. My question is: Does this also apply in descriptive complexity settings, particularly when it comes to testing a pair of SO-Horn queries to see if they describe the same language? I'm not aware of any descriptive complexity version of Rice's theorem, and I could conceivably see that it might not be all that difficult to test two second-order formulas for equivalence.

First, note that the equality of two TMs is harder than the halting problem (it is $\Pi^0_2$-complete), i.e. you can not compute it even with an oracle for the halting problem. So it is not even c.e. (i.e. $\Sigma^0_1$, a.k.a. r.e.). Rice's theorem implies that the set is not c.e., it does not imply the stronger result.
I think the question of deciding the equality of even simpler functions is co-c.e.-complete (i.e. $\Pi_1$-complete). We can not check if two multinomials are equivalent over natural numbers (since the complement is c.e.-complete by the MRDP theorem), and this implies that we cannot check the equality of two SO-Horn queries.
• Why do you describe $\Pi^0_1$ as "harder" than $\Sigma^0_1$? You can't compute the halting problem with an oracle for TM equality either: they're incomparable. Dec 20 '10 at 5:12
• @Mark Reitblatt: that was a typo, it should be $\Pi^0_2$-complete because there is an existential quantifier for computation and it is unbounded. Thanks for noticing it. I will fix it. (ps: you can decide halting using an oracle for equality, it is an easy exercise.) Dec 20 '10 at 6:11