The halting Problem states that there is no Turing Maschine that is able to decide whether an arbitrary other Turing Machine will halt.
In 2016 Adam Yedidia and Scott Aaronson presented a turing machine whose behaviour is independent of ZFC. Meaning, they gave a specific Turing Maschine $Z$ for which it is impossible (assuming ZFC is consistent) to decide whether $Z$ halts or not. This Turing Maschine has 7912 states.
Yedidia now argues, that by using the value of the Busy Beaver Function $\sum(7912)$, one can get the maximum number of timesteps for which one needs to run any 7912 state Turing Machine, in order to know whether it will halt or not. However, that would allow to know whether $Z$ halts (by running it for $\sum(7912)$ timesteps), which is impossible as they showed. Thus, our assumption, the number $\sum(7912)$ can be obtained using just ZFC, must be wrong. Only by using stronger Axiomatic systems (i.e. "$ZFC^+$") one might be able to obtain $\sum(7912)$ and thus decide whether $Z$ will halt. This gives a number for an upper bound on the strength of ZFC $P(ZFC) < 7912$.
My Question now is the following:
-
There seems to be (a/some) ordering of axiomatic systems which rank them according to their strength $P$ (in the above sense). i.e. something like $P(ZFC) < 7912$ while $P(ZFC^+)>P(ZFC)$. Is this correct?
-
Assuming we have an axiomatic system $X$ which is in some sense the weakest axiomatic system possible and we have a smalest Turingmachine $Z_x$ for which $X$ can not decide whether $Z_x$ will halt. What can we say about $X$ or $Z_x$? I'm interested in literally anything related to that notion as I'm kind of stuck while googling.
-
What do we know about the next more powerfull axiomatic system? Can we get Axioms $X$ with $P(X) = c$ of any natural number $c\in \mathbb{N}$?
Please feel free to point me to a more appropriate place to ask this question.
Best Answer
There's not really a good notion of "weakest axiom system" that behaves well in this case. The absolute weakest axiom system (in some appropriate language - e.g. of set theory or of arithmetic) is the "empty theory" $E$, which is the system with no axioms at all - just the inference rules of first-order logic. However, it doesn't really make sense to ask what $E$ proves about Turing machines because in some sense it's not strong enough to even talk about them meaningfully. For example, the statement "Adding 'dummy states' to a Turing machine doesn't affect its halting behavior" isn't provable in the empty theory.
So we'd want to restrict attention to theories which are strong enough to prove "basic facts" about Turing machines; it's also reasonable to shift from set theories (which by nature are generally quite powerful) to arithmetics. At this point however the notion of "weakest appropriate system" becomes rather fuzzy - reasonable candidates include Robinson arithmetic towards the bottom and $I\Delta_0+Exp$ much stronger but still quite weak; Hajek/Pudlak's book The metamathematics of first-order arithmetic is an excellent reference on the strengths of various systems around this level.
Now as to the notion of $P(T)$ for $T$ an "appropriate" theory, the right definition is the following:
An important issue here unfortunately is that $P$ - and all related functions, like "the least $n$ such that $\Phi_n(n)$ doesn't halt but $T$ doesn't prove that" - is highly model-dependent: different models of computation can yield very different answers (for example, we can whip up an artificial but perfectly well-behaved model for which $P(T)$ is never a multiple of $17$ as long as $T$ is "reasonable"). This lack of robustness is why the specific values of $P$ are not generally thought of as particularly interesting. Aaronson/Yedidia showed that $P(ZFC)$ is much more tractable than one might reasonably guess, but the particular value of the bound they get isn't (in my opinion) interesting on its own.
It's also worth noting that $P$-value isn't related with actual strength beyond the obvious fact that $P(T_1)<P(T_2)$ implies $T_1\not\supseteq T_2$: there are theories $T_1,T_2$ such that neither contains the other but with $P(T_1)<P(T_2)$.
All of the above being said, here are a couple ameliorating points:
There is a more subtle connection between $P$-values and logical power, via consistency strength. Suppose $T_1,T_2$ are "reasonable" theories such that $T_1$ proves that $T_2$ is consistent. Then $P(T_1)\ge P(T_2)$: since $T_1$ proves the consistency of $T_2$ we have that $T_1$ also proves that every $\Pi_1$ theorem of $T_2$ is true, but non-halting claims are $\Pi_1$ so whenever $T_2$ proves that a machine doesn't halt $T_1$ must also prove that.
While I've treated it as a negative above, model dependence could also raise some interesting questions - namely, questions of the form "Is there a model of computation according to which $P$ has such-and-such property?" At present, though, I don't know a particularly interesting example. But I'm sure one exists. (As supporting evidence, for an example of an interesting result about "special models of computation" consider the existence of Friedberg enumerations; this isn't about $P$, but it demonstrates that some fairly concrete questions can have interesting and surprising answers.)