Formula $\Sigma_{1}$ in $Q$ but not $\Sigma_{1}$ A formula $\varphi$ is $\Sigma_{1}$ over a given theory $T$ if $T\vdash \varphi \leftrightarrow \psi$ for some $\psi \in \Sigma_{1}$.
Is there a formula $\varphi$ in the language of arithmetic that is $\Sigma_{1}$ over (Robinson's) $Q$ but not $\Sigma_{1}$? What about one that is $\Sigma_{1}$ over $Th(\mathbb{N})$ but not over $Q$? Please provide examples, if possible.
 A: Note that, in general, every axiom of $T$ is equivalent to the quantifier-free formula $0=0$ under the definition you have given. So for the first question it is sufficient to find any axiom that is not logically equivalent to a $\Sigma^0_1$ formula. 
There is such an axiom for $Q$, namely $(\forall y)(y = 0 \lor (\exists x)(y = S(x)))$. This axiom is $\Pi^0_2$ and it cannot be logically equivalent to a $\Sigma^0_1$ formula because it is not preserved under taking superstructures. 
The fact in my first paragraph also gives information on the second question, because it means that any arithmetical formula that is true in $\mathbb{N}$ is $\Sigma^0_1$ over $\operatorname{Th}(\mathbb{N})$. So all you need for the second question is a formula true in $\mathbb{N}$ but not equivalent to a $\Sigma^0_1$ formula over $Q$. 
Furthermore, because $Q$ proves any true $\Sigma^0_1$ formula, it is sufficient to find any arithmetical formula that is true in $\mathbb{N}$ but not provable in $Q$. Because if a true formula $\phi$ was provably equivalent over $Q$ to a $\Sigma^0_1$ formula, then because the axioms of $Q$ are true the $\Sigma^0_1$ formula would be true, hence provable in $Q$, and thus $\phi$ would also be provable in $Q$.  One concrete example of a true formula not provable in $Q$ is the Paris--Harrington principle. 
A: Yes, there are.
For the first question, let $\varphi(x) \in \Sigma_1$. Let $\varphi'(x)$ be $\varphi(x) \land \forall x\ (x=x)$.
For the second question, take an arbitrary formula $\varphi(x) \in \Sigma_1$. Let $T$ be a consistent recursively axiomatizable theory containt Robinson's $Q$. Let $\psi(x)$ be a formula that is true for all natural numbers (i.e. $\mathbb{N} \vDash \forall x \ \psi(x)$) but is not provable in $T$. Let $\varphi'(x)$ be $(\varphi(x) \land \psi(x)) \lor (\lnot \varphi(x) \land \lnot \psi(x))$. It is clear that $\mathbb{N} \vDash \forall x \ (\varphi(x) \leftrightarrow \varphi'(x)$. On the other hand $T \nvdash \forall x \ (\varphi(x) \leftrightarrow \varphi'(x))$ since that would imply $T \vdash \forall x \ \psi(x)$. Edit: This only shows that $\varphi'$ is not equivalent to the original formula, not that it is not provable $\Sigma_1$. 
I think the answer is still yes since a no answer would imply  that the set of $T$-provably $\Sigma_1$ formulas are effectively enumerable which I think is false. But I don't have a short poof for it or a reference. I will update the answer when I find it. (still I think there should be an easier proof).
