In this question, it was mentioned that there are descriptive complexity versions of Rice's theorem. I found a proof of the following theorem:
Given a complexity class C, nontrivial properties of languages in C cannot be computed in C
I had previously posted the proof I found, but because it was so long and because it was pointed out in the comments that this paper contains a proof of that theorem already, I removed it. (If for some reason you are desperate to see my proof, please see the previous revisions of this question.)
My interest is in whether or not this theorem could be used to separate AC0 and PSPACE. Here's the argument:
Consider the property P of the complexity class AC0 defined as follows:
P: the property of being an FO query that accepts a particular fixed structure, namely the structure consisting of one element, no functions, no constants, and no relations
Clearly, by the theorem above, P is not decidable in AC0; it is a non-trivial property of FO queries.
However, a little examination should show that computing whether or not an FO query accepts such a simple structure can be decided as easily as TQBF; thus, P is decidable in PSPACE.
To ensure clarity on this point (that P is computable in PSPACE): Note that the property we are interested in requires that the structure be FO. So, we are trying to determine whether a FO query that is running on a single-element structure with no relations accepts. Because there are no relations to deal with, it should be clear that the task of deciding such an FO query is equivalent to deciding an instance of TQBF; there are no relations, so the only challenge that remains is to evaluate whether or not the quantified boolean formula is true. This is basically just TQBF, so P is computable in PSPACE.
Because P is computable in PSPACE but not AC0, we should be able to conclude that AC0 != PSPACE. Is this reasoning correct, or have I made a mistake somewhere? I'm particularly concerned about the preceding paragraph; I'll try to clarify and update the argument tomorrow after I get a chance to give a little more thought to the exposition.
I would accept as an answer an example of a FO query that, when computing on the one-element, relation-free structure I've described, clearly does not make sense as an instance of TQBF. (I'm suggesting that there isn't one, so if you can show that there is one, that would be a counterexample.)