How can we express "$P=PSPACE$" as a first-order formula? How can we express "$P=PSPACE$" as a first-order formula?
Which level of the arithmetic hierarchy contains this formula (and what is the currently known minimum level of the hierarchy that contains it)?


For reference, see this blog post by Lipton.
Firstly, I want to address the comments to the question, where it was suggested that "false" expresses $P = PSPACE$ because the statement is false. While this might be a good joke, it is actually very much harmful to think this way. When we ask how to express a certain sentence in a certain formal system, we are not talking about truth values. If we were, then when someone asked "How do I write down the fact that there are infinitely many primes?" we could answer "3 + 3 = 6", but this clearly will not do. For the same reason "false" is not a valid answer to "how do I write down $P = PSPACE$?". I think Frege and Russell tried hard to teach us that lesson. Ok, now to the answer.

Let me show how to express $PSPACE \subseteq P$, the other direction is similar, and then you can put them together in a conjunction to get $PSPACE = P$. In any case, for your purposes it may be sufficient to express just $PSPACE \subseteq P$, depending on what you are doing.

Using techniques similar to those in the construction of Kleene's predicate $T$, 
we can construct a bounded quantifer formula $accept_{space}(k, m, n)$ (which thus resides in $\Sigma^0_0 = \Pi^0_0$) saying "when we run the machine encoded by $k$ and bound its space usage to $|n|^m$, the machine accepts the input $n$." Here $|n|$ is the length of $n$. An informal way of seeing that such formulas exists is this: given $k$, $m$, and $n$ we can compute primitive recursive bound on how much time and how much space we are ever going to need (i.e., at most $|n|^m$ space and at most $2^{|n|^m}$ time). We then simply search through all possible execution traces which are within the computed bounds--such a search is rather inefficient, but it is primitive recursive and so we can express it as a bounded formula.

There is a similar formula $accept_{time}(k, m, n)$ in which the running time is bound by $|n|^m$.

Now consider the formula:
$$\forall k, m . \exists k', m' . \forall n .
accept_{space}(k,m,n) \Leftrightarrow accept_{time}(k',m', n).
$$
It says that for every machine $k$ which uses at most space $|n|^m$ there is a machine $k'$ which uses at most time $|n|^{m'}$ such that the two machines accepts exactly the same $n$'s. In other words, the formula says $PSPACE \subseteq P$. This formula is $\Pi^0_3$.

We can improve this if we are willing to express instead the sentence "$TQBF$ is in polytime" , which should be good enough for most applications, as TQBF is PSPACE complete and so it being in polytime is equivalent to $PSPACE \subseteq P$. Let $k_0$ be (the code of) a machine which recognizes TQBF in space $|n|^{m_0}$. Then "$TQBF \in P$" can be expressed as
$$\exists k', m' . \forall n . accept_{space}(k_0, m_0, n) \Leftrightarrow accept_{time}(k', m', n).$$
This formula is just $\Sigma^0_2$. If I were a complexity theorist I would know if it is possible to do even better (but I doubt it).