<p>$\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.</p>

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

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

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

<p>In general, statements of the form</p>

<blockquote>
  <p>(2) If ZFC proves $\phi$, then $\phi$.</p>
</blockquote>

<p>are known as instances of the <em>reflection principle</em> 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.</p>

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

<p>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 <em>finitistic reflection principle</em></p>

<blockquote>
  <p>(3) If $\phi$ has a ZFC-proof of length $\le s$, then $\phi$.</p>
</blockquote>

<p>This <em>is</em> 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).</p>

<p>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 <em>polynomial</em> 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)$.</p>

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

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

<p>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.)</p>

<p>[1] Pavel Pudlák, <a href="http://www.math.cas.cz/%7Epudlak/fin-con.pdf" rel="noreferrer"><em>On the length of proofs of finitistic consistency statements in first order theories</em></a>, in: Logic Colloquium ’84 (Paris, Wilkie, Wilmers, eds.), Studies in Logic and the Foundations of Mathematics vol. 120, 1986, pp. 165–196, doi: <a href="https://doi.org/10.1016/S0049-237X(08)70462-2" rel="noreferrer">10.1016/S0049-237X(08)70462-2</a>.</p>

<p>[2] Pavel Pudlák, <a href="http://www.math.cas.cz/%7Epudlak/improved.pdf" rel="noreferrer"><em>Improved bounds to the length of proofs of finitistic consistency statements</em></a>, in: Logic and Combinatorics (Simpson, ed.), Contemporary Mathematics vol. 65, American Mathematical Society, 1987, pp. 309–331, doi: <a href="https://doi.org/10.1090/conm/065" rel="noreferrer">10.1090/conm/065</a>.</p>

CC BY-SA 3.0
2018-04-20T19:13:15.787Z
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
CC BY-SA 3.0
2018-04-20T19:21:52.807Z
... 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
CC BY-SA 3.0
2018-04-21T08:07:41.283Z
Oh dear. Yes, that is an embarassing typo.
Emil Jeřábek
CC BY-SA 3.0
2018-04-20T16:02:23.687Z
2018-04-21T08:06:26.040Z
2018-04-21T08:06:26.040Z
Emil Jeřábek
<p>While reading some articles on formal proofs (see also my <a href="https://cstheory.stackexchange.com/q/39892/3247">previous question on cstheory</a> about the length of ZFC proofs versus human written proofs), I came up with this apparent paradox.</p>

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

<pre><code>Program M_const( M )
  enumerate all strings S of length  &lt;= |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 
</code></pre>

<p>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)$).</p>

<pre><code>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 // -&gt; O(n)
    otherwise halts                                // -&gt; O(1)
  some dummy unused code here  // see below
</code></pre>

<p>It is clear (and hopefully provable in ZFC) that:</p>

<ol>
<li>$M_{const}$ always halts and is correct;</li>
<li>if $M_{const}( M_{paradox} ) = Yes$ then $M_{const} \notin O(1)$ by construction; so we have a contradiction;</li>
<li>so $M_{const}(M_{paradox}) = No $; and we can have:

<ul>
<li>(a) $M_{paradox} \notin O(1)$ OR</li>
<li>(b) $M_{paradox} \in O(1)$ AND there is not a short proof of it;</li>
</ul></li>
</ol>

<p>but case $(a)$ cannot hold by construction; so ...</p>

<ol start="4">
<li>$M_{paradox} \in O(1)$</li>
<li>AND there is not a short proof of it;</li>
</ol>

<p>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)$ ???</p>

<blockquote>
  <p><strong>Q1.</strong> What is the output of $M_{const}( M_{paradox} )$ ?</p>
</blockquote>

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

CC BY-SA 3.0
2018-04-16T09:47:16.513Z
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
CC BY-SA 3.0
2018-04-16T11:11:33.310Z
@EmilJeřábek: Thanks! I'm not an expert, but can we add it as an axiom (and what happens)? Or derive it from (ZFC + Cons(ZFC))? And above all what is the output of M_const( M_paradox)? ... at this point it seems that the only way to get an answer is to fill in all the details and run it!
Marzio De Biasi
CC BY-SA 3.0
2018-04-16T21:50:57.837Z
@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
CC BY-SA 3.0
2018-04-16T21:53:46.097Z
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
CC BY-SA 3.0
2018-04-17T11:01:16.713Z
@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
CC BY-SA 3.0
2018-04-17T11:10:17.083Z
I realized meanwhile that the situation is even more complicated. In point 2, $M_{paradox}$ is a concrete TM encoded by a standard integer, thus the bound $|M|^2$ is also standard. This means we do not actually need the unrestricted $\Sigma_2$-reflection principle, but only a *finitistic* reflection principle of the form “if $\phi$ has a ZFC-proof of length at most $s$, then $\phi$”, where $s$ and $\phi$ are fixed standard number and formula, not universally quantified variables. This form of the reflection principle *is* provable in ZFC, but the length of its proof will depend on $s$. ...
Emil Jeřábek
CC BY-SA 3.0
2018-04-17T11:17:35.890Z
... 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 https://doi.org/10.1016/S0049-237X(08)70462-2 ; see also http://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
CC BY-SA 3.0
2018-04-17T11:20:53.160Z
@EmilJeřábek: thank you very much; I'll elaborate it later. BTW way I just added another "messed" part that hooks the paradox to P=NP ?!?
Marzio De Biasi
CC BY-SA 3.0
2018-04-17T11:20:58.603Z
... than $s$ (i.e., $|M|^2$ in your case), hence no contradiction arises. In fact, I believe that Pudlák’s lower bounds on the lengths of proofs of the finitistic consistency statements are proved using a diagonalization argument not unlike the one underlying your paradox. So, anyway: the answer is that $M_{const}(M_{paradox})$ outputs NO, and ZFC can even prove this, but it will need a long proof.
Emil Jeřábek
CC BY-SA 3.0
2018-04-18T00:17:32.997Z
As a side note, you are not really using the power of ZFC, you can replace it with PA or PRA (and probably much weaker arithmetic theories).
Kaveh
CC BY-SA 3.0
2018-04-18T00:43:06.807Z
Also Turing Machines in these arguments are probably an unnecessary detour. E.g. Godels's incompleteness argument gives a fixed point for formulas: for any A(x,y) there is a B(x) such that T proves A(x, <B>)  iff B(x). If I am not mistaken, you are essentially playing with A being nonexistence of "short" proof in T for formula encoded by y on x. So there is a fixed point formula that doesn't have one. To get an inconsistency you need to show it had one, but you really cannot do that. So in all of these kind of arguments there is a problem is that part of the argument.
Kaveh
CC BY-SA 3.0
2018-04-18T00:52:01.760Z
Intrusively it might seem there is a "short" proof in T, but when you try to write that proof down you see that it is not really "short" or used something outside T. A typical one is assuming soundness of finite proofs "if z is a T proof of formula encoded by y, then y is true" or reflection "if z is a T proof of formula encoded by <B> then B". These are not part of T. So you have to prove then. Then the question becomes what is the shortest proof of these finite soundness/reflection/consistency statements.
Kaveh
CC BY-SA 3.0
2018-04-18T00:52:45.040Z
Pavel has a considerable amount of work on these. If you are interested a good read is his recent book, in particular, iirc, chapter 6. P. Pudlák, "Logical Foundations of Mathematics and Computational Complexity, a gentle introduction", 2013.
Kaveh
CC BY-SA 3.0
2018-04-18T13:08:43.337Z
@EmilJeřábek: thanks, if you want you can convert the comments about Q1 to an answer. And see if it the same observations can be extended to Q2, but in that case I'm using an arbitrary large "concrete proof" for a single machine to prove that a short proof of it exists for infinitely many padded versions of it (which it should be provable in ZFC) and then derive the contradiction (which would ultimately imply P!=NP ;).
Marzio De Biasi
CC BY-SA 3.0
2018-04-18T14:44:19.827Z
@Kaveh: thanks; it's a great book, I bought it a few months ago but I'm proceeding very slowly in spare time and I'm still at chapter 4.
Marzio De Biasi
CC BY-SA 3.0
2018-04-20T17:24:38.780Z
As far as  can see, Q2 runs into much the same issue in that a formalization in ZFC would need to appeal to a reflection principle, and it also runs into another issue, namely that you are implicitly assuming that P = NP implies that ZFC proves that P = NP.
Emil Jeřábek
<lo.logic><time-complexity>
Formalization of proofs and computational complexity paradox?
Marzio De Biasi
# Formalization of proofs and computational complexity paradox?

(Asked by: username_0 on 2018-04-16)

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:

$M_{const}$ always halts and is correct;
if $M_{const}( M_{paradox} ) = Yes$ then $M_{const} \notin O(1)$ by construction; so we have a contradiction;
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 ...

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

**Tags:** lo.logic, time-complexity
> **Comments:**
> **username_1**: 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.  
> **username_0**: @EmilJeřábek: Thanks! I'm not an expert, but can we add it as an axiom (and what happens)? Or derive it from (ZFC + Cons(ZFC))? And above all what is the output of M_const( M_paradox)? ... at this point it seems that the only way to get an answer is to fill in all the details and run it!  
> **username_2**: @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..  
> **username_2**: 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.  
> **username_1**: @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.  
> **username_1**: I realized meanwhile that the situation is even more complicated. In point 2, $M_{paradox}$ is a concrete TM encoded by a standard integer, thus the bound $|M|^2$ is also standard. This means we do not actually need the unrestricted $\Sigma_2$-reflection principle, but only a *finitistic* reflection principle of the form “if $\phi$ has a ZFC-proof of length at most $s$, then $\phi$”, where $s$ and $\phi$ are fixed standard number and formula, not universally quantified variables. This form of the reflection principle *is* provable in ZFC, but the length of its proof will depend on $s$. ...  
> **username_1**: ... 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 https://doi.org/10.1016/S0049-237X(08)70462-2 ; see also http://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 ...  
> **username_0**: @EmilJeřábek: thank you very much; I'll elaborate it later. BTW way I just added another "messed" part that hooks the paradox to P=NP ?!?  
> **username_1**: ... than $s$ (i.e., $|M|^2$ in your case), hence no contradiction arises. In fact, I believe that Pudlák’s lower bounds on the lengths of proofs of the finitistic consistency statements are proved using a diagonalization argument not unlike the one underlying your paradox. So, anyway: the answer is that $M_{const}(M_{paradox})$ outputs NO, and ZFC can even prove this, but it will need a long proof.  
> **username_3**: As a side note, you are not really using the power of ZFC, you can replace it with PA or PRA (and probably much weaker arithmetic theories).  
> **username_3**: Also Turing Machines in these arguments are probably an unnecessary detour. E.g. Godels's incompleteness argument gives a fixed point for formulas: for any A(x,y) there is a B(x) such that T proves A(x, <B>)  iff B(x). If I am not mistaken, you are essentially playing with A being nonexistence of "short" proof in T for formula encoded by y on x. So there is a fixed point formula that doesn't have one. To get an inconsistency you need to show it had one, but you really cannot do that. So in all of these kind of arguments there is a problem is that part of the argument.  
> **username_3**: Intrusively it might seem there is a "short" proof in T, but when you try to write that proof down you see that it is not really "short" or used something outside T. A typical one is assuming soundness of finite proofs "if z is a T proof of formula encoded by y, then y is true" or reflection "if z is a T proof of formula encoded by <B> then B". These are not part of T. So you have to prove then. Then the question becomes what is the shortest proof of these finite soundness/reflection/consistency statements.  
> **username_3**: Pavel has a considerable amount of work on these. If you are interested a good read is his recent book, in particular, iirc, chapter 6. P. Pudlák, "Logical Foundations of Mathematics and Computational Complexity, a gentle introduction", 2013.  
> **username_0**: @EmilJeřábek: thanks, if you want you can convert the comments about Q1 to an answer. And see if it the same observations can be extended to Q2, but in that case I'm using an arbitrary large "concrete proof" for a single machine to prove that a short proof of it exists for infinitely many padded versions of it (which it should be provable in ZFC) and then derive the contradiction (which would ultimately imply P!=NP ;).  
> **username_0**: @Kaveh: thanks; it's a great book, I bought it a few months ago but I'm proceeding very slowly in spare time and I'm still at chapter 4.  
> **username_1**: As far as  can see, Q2 runs into much the same issue in that a formalization in ZFC would need to appeal to a reflection principle, and it also runs into another issue, namely that you are implicitly assuming that P = NP implies that ZFC proves that P = NP.  

---

## 1 answers

### Answer by username_1 on 2018-04-20. Score: 9 | Accepted answer

$\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*](http://www.math.cas.cz/%7Epudlak/fin-con.pdf), 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](https://doi.org/10.1016/S0049-237X(08)70462-2).

[2] Pavel Pudlák, [*Improved bounds to the length of proofs of finitistic consistency statements*](http://www.math.cas.cz/%7Epudlak/improved.pdf), in: Logic and Combinatorics (Simpson, ed.), Contemporary Mathematics vol. 65, American Mathematical Society, 1987, pp. 309–331, doi: [10.1090/conm/065](https://doi.org/10.1090/conm/065).

> **Comments:**
> **username_0**: 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" :-)  
> **username_0**: ... 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.  
> **username_1**: Oh dear. Yes, that is an embarassing typo.  

---

