

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer

This question already has an answer here:

Given any really large number $x$, such as the busy beaver number $x=BB(BB(99))$, can we construct a proposition such that we know it has a proof or a disproof, but we also know the shortest such proof or disproof is longer then $x$ symbols?

share|cite|improve this question

marked as duplicate by MJD, azimut, rschwieb, Rick Decker, TMM Aug 27 '13 at 18:08


Not so Git Gud. If the parentheses are put back in (say to the left), so the premiss is of the form $(\varphi \land 1 = 1)$ then exactly ONE application of conjunction elimination is needed to get the conclusion! – Peter Smith Aug 27 '13 at 16:47
One might also reasonably require that the proposition is "short" compared to $x$ itself. – Henning Makholm Aug 27 '13 at 16:48
@PeterSmith Right. Missed that. Comment deleted. Thanks. – Git Gud Aug 27 '13 at 16:50

There is a beautiful paper by George Boolos related to this, called "A Curious Inference" (in his collected papers called Logic, Logic, and Logic).

Suppose $s$ is a one-place function sign, and $f$ a two-place function sign. And take the five axioms

$\forall n \, f(n, 1) = s1$

$\forall x\, f(1, sx) = ssf(1, x)$

$\forall n\forall x\, f(sn, sx) = f(n, f(sn, x))$


$\forall x(Dx \to Dsx)$

What's going on here is that $f$ is defined to be Ackermann-like (if we think of $s$ as successor) and the last two axioms say that $D$ is hereditary down an $s$ sequence. So we'll have the likes of


But it will take in the order of Ackermann(5,5) steps to get there in first-order logic. And if that isn't a big enough number for you, just choose target

$Df(ss\ldots ss1,ss\ldots ss1)$.

so the first-order proof has the order of Ackermann($n$,$n$) steps!

Now the curious thing of Boolos's title is that while the first-order proof would have vastly more steps then particles in the known universe, we can write down a second-order derivation in a couple of pages (regimenting our informal reasoning that the conclusion does indeed follow).

share|cite|improve this answer

If you have a short definite description of $x$, then you can use Gödel's construction to create a sentence that says "I have no proof in less than $x$ symbols". This sentence has to be true, because if it was false then it would (by itself) have a short proof, and things that are false have no proofs, short or long.

However, if that sentence is true, it must be provably true, because we can "just" check all strings of up to $x$ symbols and see whether one of them happens to prove it.

The only caveat is that your description of $x$ needs to allow us to know when we have checked long enough strings. Therefore $BB(BB(99))$ is not a likely candidate, because we can't know when we've reached that number exactly. As long as your $x$ comes from a well-defined computable function you should be fine, though.

share|cite|improve this answer
What if I require that we cant construct a valid argument (as you did here) that its false or true in less then x symbols either? And why doesnt your reasoning thats its provable constitute a proof in less then x symbols? – Abdulh Khazzak Gustav ElFakiri Aug 27 '13 at 16:53
The argument contains the hidden assumption that the axiom system cannot prove falsehoods. So the argument isn't actually formalizable in the axiom system we're speaking about. – Henning Makholm Aug 27 '13 at 16:56
