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?

Flatland: A Romance of Many Dimensions"! Keep up the good work, David! :-) $\endgroup$ – Morteza Azad Aug 7 '18 at 17:08