# Lower bound on proof length

Given any positive integer $n$, is there a way to quickly construct a statement $S$, such that the shortest proof of $S$, if it exists, must have length at least $n$?

And such that one out of $S$ or not $S$, is provable.

And question 2:
If S, then a proof of S must have length atleast n.
If not S, then a proof of not S must have length atleast n.

Edit:

I had in mind that the number of symbols in S be of the same order as the number of symbols required to specify n.

-
How do you define "length" of a proof? –  Cameron Buie May 30 '12 at 23:30
Character count when everything is written down in its language. –  user1708 May 30 '12 at 23:31
That depends on what your axioms and your proof rules are. If your proof rules are such that you can establish bounds on how long a statement with a proof of length $n$ can be, then just take a very, very long statement (e.g. a conjunction of many statements). –  Qiaochu Yuan May 30 '12 at 23:42
I can't imagine it's possible for $n=1$. –  Cameron Buie May 30 '12 at 23:49
@RobertIsrael Yes, but there are interesting questions that can be asked in this setting by slight variations of what Xnyy... wrote, which I think are closer to their intention. For example, given a total recursive $f$, is there a recursive procedure that to each $n$ assigns $S_n$ of length at most ... whose proof has length at least $f(n)$ and such that ... –  Andres Caicedo May 31 '12 at 0:56

There's a famous example that I think is due to Gödel. It is analogous to the so-called "Gödel sentence" $G$ which can be interpreted to mean "$G$ has no proof in PA", and which is therefore true but not provable in PA. (Supposing that PA is consistent.)

The analogous example is a sentence $S$ whose interpretation is

$S$ cannot be proved in PA in less than one million steps.

Suppose $S$ is false. Then $S$ can be proved in PA (in less than one million steps) and therefore PA is inconsistent.

Suppose $S$ is true. Then $S$ cannot be proved in PA in less than one million steps.

So the assumption that PA is consistent leads us to the conclusion that $S$ is either unprovable, or provable but not in less than a million steps.

But there is a proof of $S$: enumerate all proofs of up to a million steps, and check each one to make sure it does not prove $S$. (This proof takes vastly more than a million steps.) So $S$ is both true and provable and its shortest proof requires at least a million steps.

Aha, I see this is discussed in Wikipedia.

-
Possibly relevant MO thread –  MJD May 31 '12 at 2:10
This is referred to as "finitistic consistency statements" in literature. –  Kaveh May 31 '12 at 5:46