I am looking for a theory $T$ and a formula $p$ such that there is a metaproof which establishes that either $T \vdash p$ or $T \vdash \neg p$, but which does not enable us to decide which of these two cases holds.

Of course, we can define an algorithm that searches the proof space for derivations of $p$ or $\neg p$ from $T$, and given that either $T \vdash p$ or $T \vdash \neg p$, we can be sure that the algorithm will terminate at some point. Considering this, what I want is that the metaproof of the decidability of $p$ in $T$ does not enable us to construct an explicit upper bound for the time this algorithm needs.

If such $T$ and $p$ can be found, I am especially interested in a case where $T$ is some well-known foundational theory (like ZFC or PA) and $p$ is some interesting – or at least intuitively meaningful – statement (and not some practically uninterpretable formula).

  • 4
    $\begingroup$ I assume that by "theory" you mean a computable set of (closed) formulas. (Otherwise you could take PA plus all true $\Pi^0_1$-formulas, or just $Th(\mathbb N)$.) $\endgroup$ – Goldstern Oct 31 '13 at 11:17
  • $\begingroup$ Yes, good point. $\endgroup$ – Marcos Cramer Oct 31 '13 at 12:49
  • 1
    $\begingroup$ A related question: mathoverflow.net/questions/74941/… $\endgroup$ – Johan Wästlund Oct 31 '13 at 14:08


Perhaps this is the kind of example you seek.

Consider the theory $T$ in the language with one unary function symbol $S$, which asserts that $S$ is a bijection of the universe with itself, and has no finite cycles. For example, this theory is true in the integers with the usual successor operation $\langle\Z,S\rangle$, and also in the model obtained by placing two or more copies of $\Z$ aside one another.

Suppose you give me any assertion $p$ in this language, no matter how complicated. I claim that we can know that $T$ decides $p$, without knowing which way, simply by pointing out that $T$ is $\aleph_1$-categorical: every model of $T$ of size $\aleph_1$ consists precisely of $\aleph_1$ many copies of $\Z$, and these are all isomorphic. It follows that the theory is complete, and so $T$ decides $p$, even though we wouldn't necessarily know initially which way it is decided. The categoricity existence proof of decidability does not seem to provide any bound on the length of the proof, although I believe that more refined analysis would provide such bounds.

Meanwhile, let me also point out that it will be difficult to say precisely what you mean by not being able to construct an explicit bound, since the function that takes an assertion $p$ to the length of the shortest proof of $p$ in $T$ is a computable function, whose program we can write down, and so our situation is that we have an explicitly given computable function that provides the bound.

Update. One can use this example to also make an example over ZFC or another foundational theory. Suppose ZFC is consistent. Fix any $p$ in the language of successor as above, but let $\varphi_p$ be the assertion "$T$ proves $p$", as formalized in the language of set theory. Now, if $T$ really does prove $p$, then we can prove $\varphi_p$ in ZFC. And if it doesn't, then $T$ proves $\neg p$, and we can prove in ZFC that $T$ proves $\neg p$, and so since ZFC proves that $T$ is consistent and complete, we can prove $\neg\varphi_p$ in ZFC. In this way, we have transformed the example above into an example in the foundational theory ZFC.

  • $\begingroup$ Thanks, this certainly responds my basic question. But still the question remains, whether we can find use ZFC or PA as our $T$, and whether we can then choose some relatively natural statement $p$. Concerning your last paragraph: In that case we don't have an explicit upper bound for the time it takes to produce the program for the function in question. Hence we still don't have an explicit upper bound for the time the algorithm mentioned in my question needs. $\endgroup$ – Marcos Cramer Oct 31 '13 at 14:21
  • $\begingroup$ I updated my answer to explain how to transform the example into a ZFC example. Concerning the program, I disagree with your remark, since we can easily write such a program explicitly. The algorithm is: on input $p$, search for a proof of $p$ or of $\neg p$. The program itself will be very short, and we can explicitly write it, and the input $p$ is given. So you are making a distinction about "explicitness" where you have an explicit program and an explicit input, but you want to say that the output is not explicit. $\endgroup$ – Joel David Hamkins Oct 31 '13 at 14:32
  • $\begingroup$ A "refined analysis" is indeed possible: The theory $T$ has elimination of quantifiers, and there is an explicit algorithm transforming any formula $\varphi$ into a quantifier-free formula $\varphi'$ which is equivalent (over $T$) to $\varphi$. Applied to any closed formula this algorithm will yield "true" or "false". $\endgroup$ – Goldstern Oct 31 '13 at 23:10
  • $\begingroup$ Proof theory can sometimes extract bounds even from proofs for which this is not obvious. Kreisel had this program of "unwinding" proofs, but I do not know if it applies to your categoricity proof. $\endgroup$ – Goldstern Oct 31 '13 at 23:12
  • $\begingroup$ Yes, indeed, what I had meant with my "refined analysis" remark was the elimination of quantifiers argument, which provides a bound on the proof. But I think this analysis does go beyond the simple categoricity argument, which is very simple. In any case, as I explain in my answer, I believe that the whole issue of explicit bounds is problematic, since we always have an explicit bound in the sense that I describe. $\endgroup$ – Joel David Hamkins Oct 31 '13 at 23:54

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.