# Formalization of proofs and CC paradox? - Part II

This was the second part of my previous question. It is very similar, and probably it has a similar answer (as Emil said in a comment), but I thought it was worth to separate it and ask it as a new one.

Definition [Padded Turing machine ] $M^z$ is a padded Turing machine of $M$ if it is equal to $M$ but has $z \geq 0$ unused unreachable states at the end of the transition table.

We define the PTIME Membership short proof ($PTMSP$) problem as:
Input: A Turing machine $M$
Question: Is there a short ZFC proof $\Gamma$ of length $|\Gamma| \leq |M|^2$ that $M$ halts in polynomial time?

$PTMSP$ is NP-complete. Quick reduction: given a 3CNF $\varphi$ build a program $M$ that on input $x$ checks if $\varphi$ (embedded in its code) is satisfiable, and if it is satisfiable loops form $1$ to $2^{|x|}$; otherwise halts. We can pad $M$ with some extra unused code in order to assure that a proof "$M$ halts in polynomial time" (which embeds as a subproof "$\varphi$ is satisfiable") would be shorter than $|M|^2$.

Then We build the following "paradox machine" $M_{pdox}$:

Program M_pdox( x )
s1.  String Me = mycode(); // ok by the recursion theorem
s2.  If x is not a padded version of Me then Halt
s3.  Get the smallest Turing machine M_i of length |M_i| < log(log(|x|))
that solves correctly the PTMSP problem on an all instances y < log(log(|x|))
after at most |M_i|^|M_i| steps
s4.  Simulate M_i( x ) for |x|^|M_i| steps // by s2. x can only be a
// padded version M_z of M_pdox
s4.1 if it outputs Yes then loop from 1 to 2^|x|
s4.2 otherwise Halt


Assumption 1. Cons(ZFC)
Assumption 2. P=NP (either provable in ZFC or added as a ZFC axiom)

It's not hard to prove (unless I'm missing something :) that:

p1. A padded Turing machine $M^z$ has the same running time of the unpadded machine $M$.

p2. If $P = NP$ then there exists a polynomial time machine $M_{PTMSP}$ that decides $PTMSP$.

p3. If $P = NP$ then soon or later $M_i$ at step s3. in the code of $M_{pdox}$ will match a padded version of $M_{PTMSP}$ and will never change; so at step s4. the (polynomial time) simulation $M_i(x)$ will correctly output $M_{PTMSP}( x)$ on all but a finite number of inputs.

p4. If there is a proof $\ell$ that $M$ runs in time $DTIME(n^k)$ then there is a proof $\ell'$ that for all $z$, $M^z$ runs in time $DTIME(n^k)$. For large enough $z_0$ we can combine such proof with the proof that $M^z$ is a padded version of $M$ (proof at most linear w.r.t. $|M^z|$) to prove that for infinitely many $z \geq z_0$ there is a short proof of length $\leq |M^z|$ that $M^z$ runs in $DTIME^k$.

p5. By construction $M_{pdox}$ runs in polynomial time or exponential time ...

p6. Suppose that $M_{pdox}$ runs in exponential time; then, by construction and the assumption $P=NP$, $M_i$ runs in polynomial time and cannot "contribute" with an exponential number of steps; so for infinitely many $M_{pdox}^z$, $M_i(M_{pdox}^z) = M_{PTMSP}(M_{pdox}^z)$ must output $Yes$, but if there is a proof that at least one $M_{pdox}^z$ runs in polynomial time, then $M_{pdox}$ must run in polynomial time, which is a contradiction.

p7. So $M_{pdox}$ must run in polynomial time (note that here, as opposed to step 2 of my previous question, the proof seems to rely on the P=NP assumption and not on reflection).

p8. Like in Q1 of my previous question, arguments p1,p2,p3,p6,p7 can be formalized to get a long proof $\Gamma_{pdox}$ that $M_{pdox}$ runs in polynomial time (and $M_{PTMSP}(M_{pdox})$ outputs $No$: $M_{pdox}$ is polynomial time but there is no short proof of it).

p9. But such proof $\Gamma_{pdox}$ implies (argument p4) that for infinitely many $z$ there is a short proof that $M_{pdox}^z$ runs in polynomial time; so for infinitely many $M_{pdox}^z$, $M_{PTMSP}(M_{pdox}^z)$ must output $Yes$, so for infinitely many $x$, $M_i(x)$ at step s4.1 will loop for an exponential number of steps, so $M_{pdox}$ must run in exponential time, which is a contradiction.

Q2 What is the output of $M_{PTMSP}( M_{pdox} )$
And what is the output $M_{PTMSP}( M_{pdox}^z )$ for large enough $z$ ?

We can also build a "super paradox" machine replacing step s4.2 otherwise halt with a search at most linear w.r.t $|x|$ for a proof of $\phi =$"$M_i( M_{pdox} )$ halts in polynomial time" and "If ZFC $\phi$ has a ZFC proof of length $< \log(\log(|x|)$ then $\phi$":

s4.2b  Spend at most |x| steps searching if there is a ZFC proof of
\phi = "M_i( M_pdox ) runs in polynomial time" and
"If \phi has a ZFC proof of length < \log(\log(|x|)) then \phi"
s4.2.1 If we find it then loops from 1 to 2^|x|
s4.2.2 Otherwise halt


Q3 Does s4.2b change anything about the paradox? (i.e. can we still say that $M_{PTMSP}( M_{pdox} )$ outputs $No$ because though $M_{pdox}$ runs in polylnomial time there is not a short ZFC proof of it?