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.

Solution 1:

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.