8
$\begingroup$

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.

  • 1
    How do you define "length" of a proof?2012-05-30
  • 1
    Character count when everything is written down in its language.2012-05-30
  • 1
    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).2012-05-30
  • 0
    I can't imagine it's possible for $n=1$.2012-05-30
  • 0
    @cameron, depends of how many mathematical new symbols do you want to define.2012-05-31
  • 0
    This surely depends on the proof system, but we have fast ways of translating between systems, so more importantly is the theory you have in mind. Are we talking of first order arithmetic and arithmetic sentences?2012-05-31
  • 0
    In most definitions of "proof", the statement being proved must appear somewhere in the proof. So any provable statement of length at least $n$ will do.2012-05-31
  • 1
    @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 ...2012-05-31

1 Answers 1

15

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.

  • 2
    [Possibly relevant MO thread](http://mathoverflow.net/questions/65282/are-any-natural-examples-of-godel-speed-up-known)2012-05-31
  • 0
    This is referred to as "finitistic consistency statements" in literature.2012-05-31