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.

| cite | improve this answer | |
  • $\begingroup$ 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. $\endgroup$ – Ewan Delanoy May 18 '13 at 11:21
  • $\begingroup$ 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$"? $\endgroup$ – fgp May 18 '13 at 11:50
  • $\begingroup$ 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? $\endgroup$ – fgp May 18 '13 at 12:14
  • 1
    $\begingroup$ 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$ ? $\endgroup$ – Ewan Delanoy May 18 '13 at 12:30
  • 1
    $\begingroup$ 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$). $\endgroup$ – Ewan Delanoy May 18 '13 at 12:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.