Could a descriptive complexity version of Rice's theorem be used to separate AC0 and PSPACE?

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.)

Thanks.

• @Kaveh: You should make your comment an answer. – Dai Le Dec 29 '10 at 19:25
• @Kaveh: Thanks for your comment. I am a little confused by what you are saying, though. Which machine in PSPACE for AC0 sets were you referring to? I was referring to the property P, which relates specifically to FO queries over very simple structures. I am suggesting that evaluating whether FO queries accept a simple structure is guaranteed to be TQBF, which is PSPACE. I don't see where a universal simulator for AC0 is needed. – Philip White Dec 29 '10 at 20:05
• @Kaveh: OK. I will prepare my attempted proof of the conjecture in this question and post it as a separate question. I thought it was correct, but I'm often wrong. (Of course, if you refute my conjecture before then, I won't bother.) – Philip White Dec 29 '10 at 21:46
• Oh. I just posted it as a question. Should I delete the new question and post it as an answer? – Philip White Dec 29 '10 at 22:17
• (I deleted it and added it to this question.) – Philip White Dec 29 '10 at 22:32

We can decide the $grU_{AC^0}$ (the graph of universal function for $AC^0$) in $PSpace$, the reason is simply that $AC^0 \subseteq L$ and we have a universal machine for languages in $L$ in $PSpace$, so it is easy to simulate the $AC^0$ machines (or the descriptive complexity equivalent of $AC^0$ which is $FO$ queries) in $PSpace$. This means that that we can decide the property you have stated in $PSpace$. Since it is a nontrivial property, it is not decidable in $AC^0$. So this argument separates $AC^0$ from $PSapce$.
But is this surprising? No, since we already know a simpler way of stating (essentially) the same argument: $AC^0 \subseteq L \subset PSpace$, the last proper inclusion is by the space hierarchy theorem.
• @Philip: yes, I think your argument is essentially right (thought you may want to recheck the definition of $FO$, the language does have non-logical symbols). – Kaveh Dec 30 '10 at 18:35
• @Philip: if I remember correctly the language of $FO$ also contains relations for order, addition, multiplication, and bit (thought some are definable from others). – Kaveh Dec 30 '10 at 20:38