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

Question

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.

Answer 1

Deciding the nontrivial properties of (an indexing) sets in a complexity class is as difficult as computing the graph of the universal function for the class. Intuitively this means that the only way to decide a nontrivial property is to simulate the machines and wait for answers. It seems to me that the idea of using such a property will just give what is known by the hierarchy theorems. (See theorem 4.2 of D. Kozen, "Indexing of subrecursive classes", 1978 for details and the exact statement of the theorem.)

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.