Formalization of proofs and computational complexity paradox?

Question

While reading some articles on formal proofs (see also my previous question on cstheory about the length of ZFC proofs versus human written proofs), I came up with this apparent paradox.

Let $M_{const}$ be a program that given Turing machine $M$ checks if there is a short ZFC proof $\Gamma$ of length $|\Gamma| \leq |M|^2$ that $M$ runs in constant time.

Program M_const( M )
  enumerate all strings S of length  <= |M|^2
    verify if S is a proof of "M in O(1)"
      if it is a valid proof the halt and accept
  if no valid proof is found halt and reject 

Now, we can build $M_{paradox}$ that knows its own code (by the recursion theorem) and on input $x$ first simulate $M_{const}( M_{paradox} )$; if it accepts then loop from $1$ to $|x|$ (so it falls in $O(n)$), otherwise halts (so it falls in $O(1)$).

Program M_paradox( x )
  String M = self_code()  // ok by the recursion theorem
  simulate M_const( M )   // simulate M_const on M_paradox
    if it accepts then for i = 1 to |x| do nothing // -> O(n)
    otherwise halts                                // -> O(1)
  some dummy unused code here  // see below

It is clear (and hopefully provable in ZFC) that:

1. $M_{const}$ always halts and is correct;
2. if $M_{const}( M_{paradox} ) = Yes$ then $M_{const} \notin O(1)$ by construction; so we have a contradiction;
3. so $M_{const}(M_{paradox}) = No $; and we can have:
   • (a) $M_{paradox} \notin O(1)$ OR
   • (b) $M_{paradox} \in O(1)$ AND there is not a short proof of it;

but case $(a)$ cannot hold by construction; so ...

4. $M_{paradox} \in O(1)$
5. AND there is not a short proof of it;

But steps 1--4 can be formalized in ZFC and (unless I'm missing something, its length depends only linearly on $|M_{paraox}|$) so we can add some dummy code to $M_{paradox}$ until such ZFC proof is shorter than $| M_{paradox}|^2$ (we can use the fact that the runtime of a Turing machine doesn't change if we add unused states, it only affects the self representation); so we get a contradiction with point 5 which says that there is not a short proof of $M_{paradox} \in O(1)$ ???

Q1. What is the output of $M_{const}( M_{paradox} )$ ?

Update: There were another question Q2 here, but it I decided to post it as a new "Part II" question to avoid confusion.

Answer 1

$\def\mc{M_\mathit{const}}\def\mp{M_\mathit{paradox}}$Let me for the record write up the answer to Q1, so that it doesn’t live only in the comments.

The reasoning given in steps 1–5 in the question is correct in the real world. Thus, $\mc(\mp)$ outputs NO, and $\mp(x)$ halts in constant time, but there is no short enough proof of this in ZFC.

When trying to formalize this argument in ZFC, the problematic step is 2: here, we need to assert, in ZFC itself, the implication

(1) If ZFC proves ‘$\mp$ halts in constant time’ by a proof of length $\le|\mp|^2$, then $\mp$ halts in constant time.

In general, statements of the form

(2) If ZFC proves $\phi$, then $\phi$.

are known as instances of the reflection principle for ZFC, and by Löb’s theorem (a generalization of Gödel’s 2nd incompleteness theorem) they are never provable in ZFC itself, except for the trivial case when ZFC already proves $\phi$. Notice that the consistency statement for ZFC is a special case of the reflection principle, for $\phi=\bot$; in general, reflection principles are strictly stronger than consistency.

In our case, $\phi$ is the $\Sigma^0_2$ formula “$\mp$ halts in constant time”, so step 2 apparently makes an appeal to the $\Sigma^0_2$-reflection principle for ZFC, unprovable in ZFC.

However, we have to our disposal an extra restriction that we ignored so far, namely that we have a bound $\le|\mp|^2$ on the length of the purported ZFC-proof of $\phi$. Crucially, at this point, $\mp$ is a fixed explicit Turing machine, hence this bound is a standard integer constant (and likewise, $\phi$ is a fixed sentence). Thus, (1) is actually an instance of the finitistic reflection principle

(3) If $\phi$ has a ZFC-proof of length $\le s$, then $\phi$.

This is actually provable in ZFC: if $\phi$ does, indeed, have a ZFC-proof of length $\le s$, then we can just take it, and derive (3) by ignoring the premise; if not, then for each string $|w|\le s$, we can “by inspection” produce a ZFC-proof that ‘$w$ is not a ZFC-proof of $\phi$’, and concatenating all these together, we obtain a proof of (3) (specifically, a proof of negation of its premise).

This brute-force proof will have length exponential in $s$, i.e., in our case, $2^{O(|\mp|^2)}$. There are in fact proofs of (3) of length polynomial in $s$ and $|\phi|$: this was proved by Pudlák [1] using efficient partial truth predicates. The improvements in [2] are only stated for consistency statements, but I believe they apply to more general reflection principles as well. Thus, there are ZFC-proofs of (1) of length $O(|\mp|^2)$.

However, this is still not enough to get a contradiction, as it seems any reasonable proof of (3) needs length more than $s$ (though the lower bounds in [1,2] are not quite that strong). Thus, ZFC-proofs of (1) will need length more than $|\mp|^2$. This cannot be fixed by raising the bounds in $\mc$ or by padding $\mp$, as these will just raise the length parameter $s$ in the same way. Thus, there is no paradox.

So, to summarize: ZFC proves that $\mc(\mp)$ outputs NO and that $\mp(x)$ halts in constant time, but the proofs are a little too long.

It is also worth mentioning that nothing in these arguments depends on ZFC specifically. The same reasoning will work for many other theories, for example Peano arithmetic. (Basically, we need a sequential theory axiomatized by finitely many axioms or nice schemata, see Pudlák’s papers for details.)

[1] Pavel Pudlák, On the length of proofs of finitistic consistency statements in first order theories, in: Logic Colloquium ’84 (Paris, Wilkie, Wilmers, eds.), Studies in Logic and the Foundations of Mathematics vol. 120, 1986, pp. 165–196, doi: 10.1016/S0049-237X(08)70462-2.

[2] Pavel Pudlák, Improved bounds to the length of proofs of finitistic consistency statements, in: Logic and Combinatorics (Simpson, ed.), Contemporary Mathematics vol. 65, American Mathematical Society, 1987, pp. 309–331, doi: 10.1090/conm/065.