# Formal systems and total programs

In this question I will work in ACA. Take any formal system $S$ with a proof verifier program that interprets classical arithmetic. Then $S$ is (arithmetically-)consistent iff some specific program $c$ (that searches for a proof of "$0=1$" over $S$) does not halt. So consistency corresponds directly to non-halting on $1$ input. Of course, it cannot correspond to halting on $1$ input, because $S$ proves the execution of every given program on an input if it halts. By the incompleteness theorem $S$ cannot prove the non-halting of $c$, which is a $Π_1$-sentence.

What about halting on all inputs? Consider the following program:

f(x):
Set m := "0".
For each pair of strings p,g of length at most |x|:
If p is a valid proof over S that g is a total program:
Set m := m+g(x).
Return m.


Clearly if $S$ is $Π_2$-sound then $f$ only runs total programs, and hence $f$ itself is total. Furthermore, $f$ dominates every function $g$ that $S$ can prove total, because $f(x)$ for sufficiently long $x$ will find that proof of totality of $g$ and hence output a longer string than $g(x)$. This also implies that $S$ cannot prove $f$ total.

Notice that this yields the incompleteness theorem for every $Π_2$-sound formal system. Also note that $f$ is computable from $S$ in the sense that there is a uniform computable translation from the proof verifier for $S$ to $f$.

Now my question is:

Is there a program computable from $S$ that is total and dominates every function that $S$ proves total, if $S$ is $Σ_1$-sound, or better still merely consistent?

If I am not mistaken, for soundness the hierarchy is $Σ_2 ⇒ Π_2 ⇒ Σ_1 ⇒ Π_1$, with $Π_1$-soundness equivalent to consistency, so there are only two levels in the hierarchy below that of $f$.

My motivation is that I am interested to know what kind of functions on natural numbers have their existence contingent on consistency or soundness of some formal system, given that we only assume predicative classical arithmetic. If $S$ has proof-theoretic ordinal $k$ with an explicit reduction function $r$ such that $\sup_{n \in ω} succ(r(x,n)) = \sup_{y \in x} y$ for every $x \in k$, then we can write a program that is provably total given that $r$ is well-founded, but dominates every function that $S$ proves total. For example, we can do this for ACA with proof-theoretic ordinal $ε_{ε_0}$, so we would have a program that is total iff ACA is consistent. But this is ad-hoc, and I want rather a uniform result for arbitrary $S$.

Edit: Sorry I actually meant to ask for functions that are not only total but also dominates all provably total functions. That was the original reason for my construction, because I read about the connection between the fast-growing hierarchy and proof-theoretic ordinals. So I have edited my question. Thanks for Noah Schweber's quick answer to my original unintended question!

• How about you replace [proof of] "$g$ is a total program" with "$g(x)$ terminates"? I think that should work for $\Sigma_1$-consistent theories (since "$g(x)$ terminates" is $\Sigma_1$). – Wojowu Aug 27 '17 at 19:30
• @Wojowu: The key feature I want is a total function that dominates all functions provably total in the given system. I can construct such under assumption of $Π_2$-soundness, and I want to know if it can be done uniformly with weaker assumptions. Note that $Σ_1$-soundness (also called 1-consistency) is not the same as consistency. I'm not sure what you mean by $Σ_1$-consistency. Deedlit mentioned in this comment that Friedman seems to suggest that my question is hard. – user21820 Aug 28 '17 at 4:02
• I understand the intent of your question, and with $\Sigma_1$-consistency I actually meant $\Sigma_1$-soundness. If in your program you replace the part "g is a total program" with "g terminates on input x" then I'm pretty sure that you get a function which is total under the assumption of $\Sigma_1$-soundness and which does outgrow all functions provably total in $S$, and that's what I meant to say in my previous comment. I can try to elaborate in an answer if you wish. – Wojowu Aug 28 '17 at 8:28
• Actually (I might be wrong on that) I think $\Pi_2$-soundness follows from $\Sigma_1$-soundness -- if we take a $\Pi_2$ sentence $\forall x:\varphi(x)$ provable in $S$, where $\varphi$ is $\Sigma_1$, then for each natural number $n$ we can deduce $\varphi(n)$. If $S$ is $\Sigma_1$-sound, this means that $\varphi(n)$ is true for each $n$, hence (by definition of truth in $\mathbb N$) $\forall x:\varphi(x)$ is true. If this is correct, then your program works for $\Sigma_1$-sound theories (since it's the same as $\Pi_2$-soundness). – Wojowu Aug 28 '17 at 9:38
• – Wojowu Aug 28 '17 at 10:47

For $\Sigma_1$-sound systems the answer is the same as in the case of $\Pi_2$-sound systems, because the two notions are equivalent. Here is an argument that $\Sigma_1\Rightarrow\Pi_2$: Consider any $\Pi_2$ formula $\forall x:\varphi(x)$, where $\varphi$ is $\Sigma_1$. Suppose this formula is proven by $S$, which is a $\Sigma_1$-sound theory. Then, for any natural number $n$, $S$ also proves $\varphi(n)$ (via logical inference). But $\varphi(n)$ is $\Sigma_1$, so by our assumption it's true in $\mathbb N$. From there it follows that $\forall x:\varphi(x)$ is true in $\mathbb N$ (by the definition of truth). Hence $S$ only proves true $\Pi_2$ sentences, i.e. is $\Pi_2$-sound.

For "merely consistent" systems we encounter a serious issue -- some functions which are provably total in $S$ might as well not be total (because we lack $\Pi_2$-soundness). Therefore requiring that some function $f$ eventually dominates every provably total function becomes a meaningless query. OP told me that this resolution satisfies them, but I have offered the following alternative:

Is there a computable function $f$ which eventually dominates all functions which are both (truly) total and provably total in $S$? (and if yes, is it possible to construct it uniformly as in the original question?)

My gut feeling (not shared by OP) is that there is some weird system which proves totality of sufficiently many functions so that no computable functions outgrows them all, but we have not found an "obvious" reason for or against its existence, so I guess we leave it as an open question for now.

• Thanks a lot! I'll leave this question open for a while in case perhaps someone who reads it may find an interesting answer to your extended question. That would really be intriguing! =) – user21820 Aug 29 '17 at 9:14

Unless I'm missing something, the answer is yes. (For simplicity I'm taking $S$ to be any consistent theory of arithmetic extending $I\Sigma_1$, just so that there's no worry about the strength of $S$.)

First, here's a computable partial function $\varphi$ which is total iff $S$ is consistent: on input $n$, halt iff $n$ is not the code of an $S$-proof of $0=1$.

Now for $\Sigma_1$-soundness, things are a bit trickier, but the same basic idea works: our partial computable function $\psi$, when given an input $n=\langle a, b\rangle$, will work as follows:

• If $a$ isn't the Godel number of a $\Sigma_1$ sentence, then we halt.

• If $a$ is the Godel number of a $\Sigma_1$ sentence, but $b$ doesn't code an $S$-proof of that sentence, then we halt.

• If $a$ is the Godel number of a $\Sigma_1$ sentence $\exists x\varphi(x)$ (with $\varphi$ having only bounded quantifiers), and $b$ codes an $S$-proof of that sentence, then we search for a $c$ such that $\varphi(c)$ is true (since $\varphi$ has only bounded quantifiers, truth = $S$-provability for $\varphi$), and halt iff we find such a $c$.

The only way for this function to not be total is if there is some $\Sigma_1$ sentence provable in $S$, which has no actual witness - that is, if $S$ is not $\Sigma_1$ sound.

(Note that in both examples above, the relevant facts about the partial computable functions in question can be proved in $S$, since we assumed $S$ extends $I\Sigma_1$. E.g. $S$ proves "$\varphi$ is total iff $S$ is consistent," hence since $S$ is consistent $S$ doesn't prove that $\varphi$ is total.)

• Sorry you are not missing anything. Obviously, I didn't think carefully enough about what I was looking for; I was looking for functions that grew faster than provably total functions. Do you mind if I edit my question? – user21820 Aug 23 '17 at 12:10