# Complexity of transforming an indirect proof into a direct one

Suppose that ZFC is consistent, and let ZFC'=ZFC+Con(ZFC). We can define a reasonable notion of the length of a proof inside ZFC', such that for any $n$ the set $P_n$ of all proofs of length $\leq n$ is finite. For any provable statement $\phi$ (I mean provable in $ZFC'$), denote by $c(\phi)$ the shortest possible length of a proof of $\phi$.

If we denote by $L_n$ the (finite) set of all provable statements written with at most $n$ characters, then
the map $f_1$ defined by $f_1(n)={\sf max}_{\phi \in L_n} (c(\phi))$ is obviously not computable (otherwise provability in ZFC' would become decidable : we would only need to browse all proofs of length $\leq f_1(n)$).

On the other hand, the map $f_2$ defined by $f_2(n)={\sf max}_{\phi \in P_n} (c(\phi))$ is certainly computable (see fgp’s answer below).

Now consider a slightly more complicated case : denote by $Q_n$ the set of statements such that there is a proof (in ZFC') of $ZFC \vdash \phi$, whose length is $\leq n$. Is the map $f_3$ defined by $f_3(n)={\sf max}_{\phi \in Q_n} (c(\phi))$ computable ?

It certainly seems so. If you pick an $\phi \in P_n$, then by definition it has a proof of length $\leq n$. Thus, $f_2(n) \leq n$, so to compute $f_2(n)$ you only have to find the smallest $m \leq n$ such that $P_m$ proves the same statements as $P_n$.
In other words, if $\Phi_i$ is the (finite!) set of statements proven by $P_i$, then $f_2$ can be defined as $$f_2(n) = \min \left\{ m \leq n\,:\, \Phi_m = \Phi_n \right\} \text{,}$$ which certainly is computable.
• You’ve indeed answered the initial question I asked, but as usual I misstated what I had in mind, I was actually thinking about another function $f_3$, I’ve just corrected the OP, sorry about that. – Ewan Delanoy May 18 '13 at 11:21
• No problem ;-) I'm not sure I get the expanded question, though. Does "There is a proof in ZFC' of $ZFC\vdash\phi$" mean "$ZFC' \vdash ZFC \rightarrow \phi$" or "$ZFC' \vdash \ulcorner ZFC \vdash \phi \urcorner$"? – fgp May 18 '13 at 11:50
• Hm, I think I get it now. What you want is to translate bounds on proof lengths from ZFC' to ZFC, right? So $f(n)=m$ expresses that if ZFC' proves $\phi$ with a proof of length $\leq n$, then ZFC proves $\phi$ with a proof of length $\leq m$ (assuming ZFC proves $\phi$ at all), right? – fgp May 18 '13 at 12:14
• Before answering more fully your questions, let me say that the main idea is this : we have an “indirect” proof of length $n$, i.e. a “proof that a proof exists”. If we convert it into a “direct” proof (and we know we can, in theory), can we control the size of the new proof in terms of $n$ ? – Ewan Delanoy May 18 '13 at 12:30
• To answer your second question : $f(n)=m$ expresses that if we a have an indirect proof of length $\leq n$, then there is a corresponding direct proof of length $\leq m$ (where “indirect proof of $\phi$” means a proof in ZFC' of $ZFC \vdash \phi$, and a “direct proof of $\phi$” means simply a proof in ZFC of $\phi$). – Ewan Delanoy May 18 '13 at 12:34