5
$\begingroup$

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

$\endgroup$
3
  • 5
    $\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, 2013 at 11:17
  • $\begingroup$ Yes, good point. $\endgroup$ Oct 31, 2013 at 12:49
  • 1
    $\begingroup$ A related question: mathoverflow.net/questions/74941/… $\endgroup$ Oct 31, 2013 at 14:08

2 Answers 2

6
$\begingroup$

$\newcommand\Z{\mathbb{Z}}$

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.

$\endgroup$
5
  • $\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$ Oct 31, 2013 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$ Oct 31, 2013 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, 2013 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, 2013 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$ Oct 31, 2013 at 23:54
1
$\begingroup$

Let $p$ state that there is no proof over PA of length at most $2^{21820}$ of the Collatz conjecture. Then clearly PA either proves $p$ or $¬p$, but we have no idea which. Furthermore, there is some evidence that Collatz-type behaviour do not have simple proofs in general, so if $p$ is true then the shortest proof of $p$ may be to simply verify all proofs of length at most $2^{21820}$, and if $p$ is false then the shortest proof of $¬p$ may be to verify some huge number of ad-hoc cases that happen to suffice for ad-hoc reasons.

Of course, this kind of example is not restricted to the Collatz conjecture. Any conjecture that sits on the border between decidability and undecidability as far as we can tell would be a good candidate for this method of generating relatively short arithmetical sentences that are provable by PA but with truth values we have no good guess for.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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