Is there a mechanical procedure within PA to reduce any ϕ to its simplest (in terms of the arithmetical hierarchy) logically equivalent form?

The question is motivated because we know that the Turing computable sets of natural numbers are exactly the sets at level $\Delta_1^0$ of the arithmetical hierarchy. We also know that the finite Ramsey theorem is provable in PA, but it is a least $\Pi_2^0$ (I am not sure about this). So, does it mean that it is logically equivalent to a $\Pi_1^0$ or $\Sigma_1^0$ formula? (because the set of Ramsey numbers is computable, right?)

Continuation from answer below: Thanks a lot, very enlightening answer! My point however was not if every P would always end up in a $\Delta_0^0$ formula, but in the lowest one that in principle could exist (not necessarily $\Delta_0^0$). The motivation is to know if every ϕ that is provable in PA, is semantically equivalent (in N) to a $\Pi_1^0$ or $\Sigma_1^0$ formula. My intuition (call it A) is that if a ϕ is provable in PA, then the set defined by it must be computable, and so should be reducible to at least a $\Delta_1^0$. Although if P exists, that would imply that we could take any ϕ, reduce it to its simplest form, and know if it is provable or not (if its simplest form is above $\Delta_1^0$, then ϕ should not be provable). My guess is that either the procedure P does not exist, or that my intuition A is wrong (or both!)

-
There seems to be a fundamental misunderstanding here somewhere. PA proves only true formulas, so if $\phi$ is provable in PA, it must be true, and therefore it is semantically equivalent to the formula $0=0$ which is $\Delta_0^0$. Formulas whose simplest form is $\Delta^0_1$ will be false for some inputs (because otherwise the simplest form would rather be the $\Delta^0_0$ formula $0=0$) and therefore such formulas are not provable. –  Henning Makholm Nov 28 '12 at 11:13

For the question in the body: Yes, any provable formula of whatever complexity is logically equivalent (given the axioms it is proved from) to $0=0$, which is even $\Delta_0^0$.

(Unless the logic the "proof" is done in is unsound, of course).

For the question in the title: No, such a mechanical procedure cannot exist, because if it did, we could use it to decide logical equivalence in general.

Suppose $\psi$ is a sentence and we want to know whether it is provable. Apply your hypothetical procedure to $$\phi(x)\;\equiv\; \psi\land (x=x)$$ Now, it $\psi$ is provable, then the output of your procedure must be a $\Delta_0^0$ formula that is true for $x=0$, and checking that is a simple mechanical matter. Conversely if $\phi$ is logically equivalent to a $\Delta_0^0$ formula that is true for $x=0$, then by Gödel's completeness theorem, $\psi$ must be is provable.

In the comment below you amend the question so it is not about "provably equivalent in PA", but "semantically equivalent in the actual natural numbers". That's actually even worse from a decidability point of view -- truth about $\mathbb N$ is if anything more slippery than provability in PA.

A mechanical procedure for simplifying formulas behaves enough like a proof system that Gödel's incompleteness theorem applies to it, and we get:

Theorem. Let $P$ be some mechanical procedure which transforms arithmetical formulas into arithmetical formulas. Assume that the output of $P$ is always semantically equivalent (in $\mathbb N$) to the input. Then there exists a formula which $P$ does not transform into a semantically equivalent formula on the lowest possible level in the arithmetical hierarchy.

Proof. Call a sentence $\phi$ "good" if $P(\phi)$ is a $\Delta^0_0$ sentence that is true. (This concept of "goodness" will take the place of "provable" in our analogy to Gödel).

Our strategy will be to produce a $\phi$ that is true but not good. Then whatever $P(\phi)$ is, it has to be something that is true, because we're assuming $P$ preserves semantics. However, $P(\phi)$ cannot be $\Delta^0_0$, because then $\phi$ would be good, which it isn't. But then $P(\phi)$ must belong somewhere higher in the arithmetical hierarchy, which means that $\phi$ is a formula for which $P$ does not produce output of minimal complexity.

In order to find such a $\phi$, introduce Gödel numbers for formulas in the usual way. Since $P$ is a mechanical procedure, and the property of being a true $\Delta^0_0$ sentence is computable, by Church-Turing and other well-known stuff there is an arithmetical formula $\psi(x)$ that is true exactly when $x$ is the Gödel number of a good formula.

Following Gödel, we can then diagonalize and produce a sentence $\phi$ whose intuitive meaning is "I am not good". (Details of this diagonalization omitted; they are somewhat confusing, not particularly enlightening, and can be found in any good exposition of Gödel's proof).

I claim that $\phi$ is not good. Namely, assume to the contrary that $\phi$ is good. Then by our assumptions on $P$, $\phi$ must be semantically equivalent to true formula -- but then $\phi$ must itself be true, and since it asserts that $\phi$ is not good, we have reached a contradiction.

Therefore $\phi$ is not good. But since that is just what $\phi$ asserts, that means that $\phi$ is true! Q.E.D.

(Essentially the same argument works if you stipulate only that $P$ preserves semantics of formulas with exactly one free variable -- just add in a vacuous "$\cdots\land(x=x)$" at appropriate places in the argument, then).

-
Thanks, I just realized that my question had not the intended meaning that I had in mind. The question would be the same, but instead of "logical equivalence" I should have asked "that defines (or is satisfied by) the same set of natural numbers". I wonder if you could answer that too! –  julian fernandez Nov 27 '12 at 18:38
I could approve your answer and ask the new one separately, if you don't know the answer! –  julian fernandez Nov 27 '12 at 18:41
@julian: Answer updated. –  Henning Makholm Nov 27 '12 at 20:45
thanks again Henning, I added a caveat in the original question, I wonder if you could address it! –  julian fernandez Nov 28 '12 at 0:09
I just realized my latter question doesn't make much sense, I found a more fundamental issue that I don't understand that I will ask separately. –  julian fernandez Nov 28 '12 at 3:17