# Is every φ above the second level of the arithmetical hierarchy independent of PA?

If I am not wrong, every $\Sigma_n$ (or $\Pi_n$ ) statement $\phi$ is equivalent to a statement that says that a given Turing machine halts (or doesn't halt) on input $C$ using a $\Sigma_{n-1}$-oracle. Then, because we do not have oracles, we shouldn't be able to prove any such statement with $n\geq 2$ within PA, even if $\phi$ is true in the standard N.

If the answer to the question is yes, does that mean that any theory stronger than PA that proves a $\phi$ true in N (but independent of PA) equivalent to introducing axioms about oracles? Are then math theories (or formal systems) stronger than PA ontologically equivalent to educated guesses about oracles?

Bonus question: Is the CH or any other axiom of set theory and beyond equivalent to some kind of transfinite halting question using some kind of "super" oracle?

More distilled question: I agree that even if ϕ is independent from PA, ϕ∨¬ϕ is not, because it is a tautology. Then, for instance, if ϕ∨¬ϕ is Σ3, then ϕ∨¬ϕ is equivalent to state that a given Turing machine halts on input C using a Σ2-oracle (and that will be true). Now, does the fact that we were able to prove ϕ∨¬ϕ mean that the oracle is not necessary? or stating it in a different way, doest it mean that, even if ϕ∨¬ϕ is Σ3, and because it can be proved, it is also equivalent to state that the same Turing machine will halt on input C even without an oracle?

-

You can certainly prove statements in PA of arbitrarily high quantifier complexity. For example, every instance of $\phi \lor \lnot \phi$ is provable in PA, regardless of the quantifier structure of $\phi$. Similarly, the induction scheme in PA contains formulas that are arbitrarily high in the arithmetical hierarchy.
The continuum hypothesis is (equivalent to) a $\Sigma^2_1$ formula. Thus you can indeed view it as solved by the "super oracle" that is able to decide this kind of type 2 quantification, namely existential quantifiers over functions from $\omega^\omega$ to $\omega$ applied to formulas of second-order arithmetic with variables for such functions. But at that level we are very, very far from "computability" in the usual sense.
I am confused now (I mean, more than before): if we can prove $\phi \lor \lnot \phi$ for any $\phi$ (which I agree) what is the meaning Post's theorem? I mean, does it mean that there are oracles that we can "know", I mean solve a non-computable halting problem? –  julian fernandez Nov 13 '12 at 19:27
Just because we can prove $\phi \lor \lnot \phi$ does not mean in general that we can prove $\phi$ nor that we can prove $\lnot \phi$. Post's theorem shows, among other things, that if we just look at the formulas that are $\Sigma^0_n$ for some $n$ then the oracle $\emptyset^{(n)}$ is able to compute the set of such formulas that are true in the standard model. But there is no way to compute that oracle by just searching through proofs. –  Carl Mummert Nov 13 '12 at 20:16
Indeed for an independent $\Sigma^0_1$ sentence $\psi$, we will be able to prove $\psi \lor \lnot \psi$ but not able to prove $\psi$ itself nor prove its negation. So whether this sentence is true in the standard model - which is what the oracle $\emptyset'$ can tell us - we cannot discover it by searching through all the proofs. –  Carl Mummert Nov 13 '12 at 20:19
An example of a nontrivial statement provable in PA is this finite version of Ramsey's theorem: for every $k$ and $M$ there is an $N$ such that for every $k$-coloring of the natural numbers from $1$ to $N$ there are at least $M$ numbers in that range which receive the same color. That statement takes some work to express as a formula in the language of arithmetic, but just looking at the quantifiers in English shows it is at least $\Pi^0_4$. –  Carl Mummert Nov 15 '12 at 16:18