Complexity of $[\forall^*] \cap Th(\langle \mathbb{N},= \rangle)$ I can prove that the decision problem of $[\forall^*] \cap Th(\langle \mathbb{N},= \rangle)$ is in coNP. However, the argument to show coNP-hardness for $[\forall^*] \cap Th(\langle \mathbb{N},= \rangle)$ is not clear to me.
To be clear the set is the set of first order sentences that in prenex normal form have only universal quantifiers and that furthermore are true under the model of naturals with equality.
Also, here is the proof I had in mind for it being in coNP.
$$
Th_{\forall^*}(\langle \mathbb{N}, = \rangle)^c = 
 \{\langle \forall x_1. \ldots\forall x_n. \psi\rangle. \langle \mathbb{N}, = \rangle \nvDash \forall x_1. \ldots\forall x_n. \psi\} = 
 \{\langle \forall x_1. \ldots\forall x_n. \psi\rangle. \langle \mathbb{N}, = \rangle \vDash \exists x_1. \ldots \exists x_n. \lnot \psi\}
$$
this last is equivalent to deciding $Th_{\exists^*}(\langle \mathbb{N}, = \rangle)$ which is NP-complete.
 A: It seems to me that your upper bound of $\mathsf{NP}$ is incorrect: in fact, $Th_{\exists^*}(\mathbb{N};=)$ (this notation matches a pattern I'm more familiar with, and is a bit shorter, so I'll use it) is $\mathsf{NP}$-hard.
We can embed $\mathsf{SAT}$ in $Th_{\exists^*}(\mathbb{N};=)$ by replacing propositional atoms with equality facts. Specifically, given a propositional sentence $\varphi$ with propositional atoms $p_1,...,p_n$, we build a $\exists^*(=)$-sentence $\hat{\varphi}$ as follows. The form of $\hat{\varphi}$ is $$\exists x^1_1,x^1_2,x^2_1,x^2_2,...,x^n_1,x^n_2(\theta)$$ where $\theta$ is the formula gotten from $\varphi$ by replacing each $p_i$ with "$x^i_1=x^i_2$." We have that $$\varphi\in\mathsf{SAT}\quad\iff\quad\mathcal{M}\models\hat{\varphi}$$ for every structure $\mathcal{M}$ with at least two elements: essentially, each witness $\nu$ to the satisfaction of $\hat{\varphi}$ in such an $\mathcal{M}$ corresponds to a satisfying truth assignment for $\varphi$ (think about whether $\nu$ makes $x^i_1=x^i_2$ or not) and conversely.
Since $Th_{\exists^*}(\mathbb{N};=)$ is $\mathsf{NP}$-hard, the problem you're interested in is $\mathsf{co}$-$\mathsf{NP}$ hard.

EDIT: Per the OP's comment below, let me expand on the last paragraph above in more detail.
Suppose $A$ reduces to $Th_{\exists^*}(\mathbb{N};=)$ via a function $f$. Then, using the completeness of $Th(\mathbb{N};=)$, $f$ yields a reduction $\hat{f}$ of $\overline{A}$ to $Th_{\neg\exists^*}(\mathbb{N};=)$: simply set $\hat{f}(\alpha)=\neg f(\alpha)$. (The general principle here is that if $T$ is a complete theory we get a computational equivalence between $\overline{T\cap\Gamma}$ and $T\cap\neg\Gamma$ for any syntactic class $\Gamma$.)
Now we can translate quickly between $Th_{\neg\exists^*}(\mathbb{N};=)$ and $Th_{\forall^*}(\mathbb{N};=)$ since the process of "pushing a negation inside a quantifier" is computationally simple (specifically, the two classes are linear-time equivalent). So this in turn means that $\overline{A}$ reduces to $Th_{\forall^*}(\mathbb{N};=)$. In particular, whenever $\mathsf{C}$ is a complexity class such that $Th_{\exists^*}(\mathbb{N};=)$ is $\mathsf{C}$-hard we know that $Th_{\exists^*}(\mathbb{N};=)$ is $\mathsf{co}$-$\mathsf{C}$-hard.
And of course there's nothing special here about $(\mathbb{N};=)$; this general idea works for $Th(\mathcal{M})$ for any structure $\mathcal{M}$.
