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.

There is a complexity theoretic version of Rice's theorem (by D. Kozen), but that gives a weaker result, which is expected, we can check non-trivial properties if we know that the machine halts, e.g. we can check if the machine accepts when run on an empty tape. Intuitively the result says (kind of) that the only way to check non-trivial properties of language of TMs is to simulate the machines (if I remember correctly).

Descriptive complexity does not change things, so I think you can ignore it and just replace it with the TMs with polynomial clocks (they can be converted to descriptive complexity characterization and descriptive complexity characterization can be converted to characterization using TMs). 

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.