# Formalization of proofs and computational complexity paradox?

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 ...

1. $M_{paradox} \in O(1)$
2. 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.

• You can't prove in ZFC that point 2 leads to contradiction. This would require the $\Sigma^0_2$-reflection principle for ZFC, which is not provable in ZFC itself by Gödel's theorem. – Emil Jeřábek Apr 16 '18 at 9:47
• @MarzioDeBiasi if you switch to working with a stronger metatheory then you don't get a desired contradiction.. In the worst case you construct a TM which cannot be shown to be O(1) in ZFC but can be shown to be in a stronger system. Just like check if n is a proof that con(ZFC); increment and loop if not else halt cannot be shown to terminate in ZFC if it's consistent.. – Daniel Gratzer Apr 16 '18 at 21:50
• The real root of the "contradiction" hinges on being able to internalize provability of the system system you're working in (so that we can talk about finding proofs with a TM) and a soundness theorem telling us that this internalized provability proving false never happens. But this is not something you can do in a reasonable metatheory. – Daniel Gratzer Apr 16 '18 at 21:53
• @MarzioDeBiasi To answer the questions: (1) You can add it as an axiom, but as jozefg explained, this will not help, as the seeming paradox only arises when you use the same theory and metatheory. (2) No, reflection principles are strictly stronger than consistency statements. They are, however, beasts with similar properties. (3) In the real world, the output will be “No”, by the argument you gave in the question. However, this will not have a suffucuently short proof in ZFC. – Emil Jeřábek Apr 17 '18 at 11:01
• ... The brute force proof will involve enumerating all strings of length $\le s$ and checking if any of them is a ZFC-proof of $\phi$; this will have length exponential in $s$. Using efficient partial truth predicates, one can show that there are in fact proofs of the finitistic reflection principles of length essentially linear in $s$ (due to Pudlák doi.org/10.1016/S0049-237X(08)70462-2 ; see also users.math.cas.cz/~pudlak/inco.pdf . The papers concentrate on consistency statements, but one can treat reflection principles the same way.) But even then, the proof is longer ... – Emil Jeřábek Apr 17 '18 at 11:17

$\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  using efficient partial truth predicates. The improvements in  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.)

 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.

 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.

• Thanks, already upvoted! But when you say "..to summarize: ZFC proves that $M_{const}(M_{paradox})$ outputs YES ... " is it a typo? (it should be "it outputs NO, $M_{paradox}$ runs in constant time, but there is no short proof" like you said in the comments?!?). Now I'm thinking how the hell it can be applied to Q2: "$M_{PTMSP}( M_{pdox} ) = No$, $M_{pdox}$ runs in polytime but there is only a long proof $\ell$ of it" seems ok, but I don't realize why $\ell$ can't be combined with "running time doesn't change with padded code" to get exists a short proof for "$M_{pdox}^z$ runs in polytime" :-) – Marzio De Biasi Apr 20 '18 at 19:13
• ... or better to derive "for infinitely many $z$ exists a short proof that $M_{pdox}^z$ runs in polytime" which is the sentence used to derive the contradiction. – Marzio De Biasi Apr 20 '18 at 19:21
• Oh dear. Yes, that is an embarassing typo. – Emil Jeřábek Apr 21 '18 at 8:07