Proof as a Σ₁ approximation to truth: what about higher degrees?

Question

Let us posit that the goal of mathematics is to study mathematical truths, and let us stick to arithmetic for simplicity: so let $\mathscr{T} \subseteq \mathbb{N}$ be the set of (Gödel codes of) true statements of arithmetic (i.e., the diagram of $\mathbb{N}$). Of course, $\mathscr{T}$, being universal $\Sigma_\omega$, is too complex to be studied directly (at least in a physical universe where the Church-Turing thesis only allows us to effectively enumerate $\Sigma_1$ sets): so instead, we pick a (recursive!) set of axioms, say maybe $\mathsf{PA}$ (first-order Peano arithmetic), that is arithmetically sound, and we study the set $\mathscr{P}$ of provable statements (theorems) of that theory, which is only $\Sigma_1$, and which provides an "approximation" to $\mathscr{T}$ in the sense that $\mathscr{P} \subseteq \mathscr{T} \subseteq \mathscr{P}^\neg$ where $\mathscr{P}^\neg$ is the ($\Pi_1$) set $\{A : \neg A\not\in\mathscr{P}\}$ of irrefutable statements. So we have an upper and lower approximation to $\mathscr{T}$ by sets of lower computational content and therefore more susceptible to study.

Preliminary question: Is there some precise sense in which we can say that $\mathscr{P} \subseteq \mathscr{T} \subseteq \mathscr{P}^\neg$ is the "best possible" approximation of $\mathscr{T}$ by $\Sigma_1$ and $\Pi_1$ sets?

Evidently, it can't be the best possible in a fixed and absolute way, because simply by adding new axioms to the theory (and Gödel tells us there are always more to add) we can get better approximations. But maybe there is a way to formalize the idea that the whole process of taking a fixed theory and using the set $\mathscr{P}$ of consequences of that theory is the best we can hope to do; and maybe even there is a way to formalize the idea that $\mathsf{PA}$ is the best theory subject to certain constraints?

Anyway, the above isn't really my question, it's just something that would help clarify my real question:

Main question: For $k\geq 2$ (maybe say $k=2$ for definiteness) is there a $\Sigma_k$ set $\mathscr{P}_k$ such that $\mathscr{P}_k \subseteq \mathscr{T} \subseteq \mathscr{P}_k^\neg$ is an "analogous" approximation to $\mathscr{T}$ at the $\Sigma_k$ level?

("Analogous" should be understood in the sense of the preliminary question. But maybe the preliminary question doesn't admit a rigorous answer, in which case, of course, "analogous" should be interpreted intuitively.)

One candidate I can think of is to define $\mathscr{P}_2$ as the set of first-order logical consequences of the set of all true $\Pi_1$ statements of arithmetic. Is this somehow the $\Sigma_2$ analogue of $\mathscr{P}$?

Let me close with a (slightly humorous) motivation for the question: suppose I want to write a science-fiction story that takes place in a universe where the Church-Turing thesis holds "up one degree", i.e., for $\mathbf{0}'$. Say the inhabitants of this universe have the ability, in constant time (in their head), to decide whether a Turing machine halts (or equivalently, whether a $\Sigma_1$ statement is true). The inhabitant of this fictional universe would presumably include mathematicians: what would such mathematicians do? and how would they approach the determination of arithmetical truth comparably to the way we use provability-from-axioms to approach it at our level?

Answer 1

One way of thinking about this problem is to think of the natural numbers as a discrete ordered semi-ring satisfying the least number principle (every non-empty subset has a least element).

There is a sense in which Peano Arithmetic is the "right" $\Sigma _1$ approximation to truth in $\mathbb{N}$: it has exactly the axioms needed to ensure the least number principle holds for every first-order definable subset. A strictly weaker $\Sigma_1$ theory would have to fail to prove the least number principle for some definable set.

However, Peano Arithmetic is not strong enough to know which definable sets are non-empty. If a $\Sigma_1$-definable set is not-empty $PA$ proves it is non-empty, but the same is not true for $\Pi_1$-definable sets. The kind of strengthenings of PA you might consider to decide some Godel sentences are essentially just adding axioms saying that particular $\Pi_1$-definable sets are non-empty (which now allows you to apply the least number principle). But these stengthenings, while "better" in one sense, are not the "right" $\Sigma_1$ approximation to truth, because they are assuming things that we can't really know without access to an oracle: like that $PA$ is consistent. One way to say this in the terminology of philosophy of science is that $PA$ consists of exactly the verifiable truths of arithmetic (those which you could, hypothetically, build a machine to verify).

If your metaphysics allows you access to the $0^{(n)}$ (the n-th iterate of the halting set), then all a sudden the verifiable truths of arithmetic grow to include for any non-empty $\Sigma_{n+1}$-definable set that this set is in fact non-empty.

$\Sigma_{n+1}$ definable sets are exactly the $\Sigma_1(0^{n})$ ($\Sigma_1$ relative to the n-th iterate of the halting set). So one way of thinking about your second question is to imagine that in addition to having a mechanical means of performing addition, multiplication, and comparing order in arithmetic, we also have a mechanical means of performing computations relative to $0^{(n)}$. We might then add a new predicate symbol to the language of arithmetic for $0^{(n)}$, since of course our language should be able to express as primitive everything we can do mechanically. And we add to our theory all of these primitive facts about which numbers are in $0^{(n)}$. Now the same argument works again: the $\Sigma_1(0^{(n)})$ (i.e., $\Sigma_{n+1}$ in the original language of arithemtic) definable non-empty sets are precisely the sets which are verifiably non-empty if non-empty. Any stronger theory would have to be making use of information we don't really have a way of verifying.

So to answer your question: the notion of scientific verifiability is makes PA the "right" theory. If we change our assumptions about what is scientifically verifiable, we get get a new "right" theory.