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

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?

• May I suggest $P \subseteq T \subseteq P^I$ as easier to read notation for these sets? – Matt F. Aug 7 '18 at 15:16
• You can also get ideas for your story from Russell Impagliazzo’s five worlds in “A Personal View of Average-Case Complexity” – Matt F. Aug 7 '18 at 15:19
• (+1) Enjoyed reading this nice imaginative question! Particularly the last paragraph which somehow reminded me of E. A. Abbott's novel "Flatland: A Romance of Many Dimensions"! Keep up the good work, David! :-) – Morteza Azad Aug 7 '18 at 17:08
• Haven't you already answered your question with your candidate? Since you haven't formalized what counts as success, it would seem difficult either to object or improve upon it. – Joel David Hamkins Aug 7 '18 at 18:39
• @JoelDavidHamkins Let's say I don't see any reason why there isn't an "obviously better" candidate, so I can't rule out someone answering (at least partially) by saying "the following $\Sigma_2$ subset of $\mathscr{T}$ is an obviously better approximation"; and conversely, there may be some good reason, if not completely formalizable, why the candidate I propose is "right". But indeed, I also can't rule out the possibility that my question has no satisfactory answer. 😕 – Gro-Tsen Aug 7 '18 at 18:50

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.

• "that PA consists of exactly the verifiable truths of arithmetic (those which you could, hypothetically, build a machine to verify)" --- this seems like a misleading way to summarize the previous comment. (PA proves that there are infinitely many primes: is this something you could, hypothetically, build a machine to verify?) – Nik Weaver Aug 7 '18 at 20:15
• We can build a machine which takes $n$ and outputs a prime bigger than $n$. Perhaps verfiability is the wrong word. – James Aug 7 '18 at 20:25
• I find it difficult to think of a (non-trivial) meaning for "things we can know without access to an oracle" that would exclude "PA is consistent" but would include all the induction axioms of PA for arbitrarily complex arithmetical formulas. (The reason I wrote "non-trivial" is that, of course, one could take provability in PA as one's criterion for oracle-less knowability, but that would make any resulting claim about a special status for PA circular.) – Andreas Blass Aug 7 '18 at 22:27
• Of course circularity is a problem if you try to completely formalize this notion. The idea would be that certain machines (or machines that create machines, or machines that create machines that create machines) will serve essentially as physical Skolem functions. The existence of such a machine, together with a proof of its correctness, can constitute a verification of a formula, even if it has many alternations of quantifiers. The circularity comes, as you point out, from the fact that PA would probably be the theory we use to prove correctness of such machines. However, it could be argued – James Aug 8 '18 at 3:27
• (cont'd) that we have some prior knowledge of how to prove things about such machines. E.g., it seems humans have the ability to see that many different hypothetical adding machines are all equivalent. The axioms of PA minus induction maybe could be considered "obvious", and constitute background assumptions (which exist in all fields of science). Most people have a pretty clear understanding of why the least number principle is true: every natural number can be reached by adding 1 to itself multiple times, and there must be a first such number in any non-empty set we can define, – James Aug 8 '18 at 3:35