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.
 A: 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.
