Allow me to muddy the waters a little bit. Before we start making statements about the lengths of proofs, we should first formally define what a proof *is*. For that, we want the concept of a *proof system*.

## What is a proof system?

A proof system is a Turing machine which runs in polynomial time and defines a function $f$ taking ordered pairs $(\varphi,p)$, where $\varphi$ is a formula and $p$ is some binary string purporting to be a proof of $\varphi$, to the set $\{V,I\}$ ($V$ for Valid, $I$ for Invalid). It is *sound* if it never returns $V$ unless $\varphi$ is actually a tautology, and it is *complete* if for every tautology $\varphi$ there is a proof $p$ with $f(\varphi,p) = V$.

## How do I check whether a proof system is sound?

In general you can't, by an easy reduction to the Halting Problem. (Start with a sound proof system, and modify it by first simulating some other program $X$ for $n$ steps, where $n$ is the length of the binary representation of $\varphi$. Output $V$ if $X$ halts within $n$ steps, otherwise run the original sound proof system.)

## Is there a "best" sound proof system?

Nobody knows? If I am interpreting this paper correctly, the naive proof system - ordinary proofs in propositional logic - has trouble proving special cases of the Pigeonhole Principle in less than exponential time. (**Edit:** I think I was misinterpreting - the Pigeonhole Principle is hard to prove when you restrict yourself to "bounded-depth Frege proofs".)

A better proof system might be the following: a valid proof $p$ of the statement $\varphi$ consists of an ordered triple $(M,q,r)$, where $M$ is a proof system, $q$ is a binary string encoding an ordinary proof in first order logic that the axioms of ZFC imply $M$ is sound, and $r$ is a proof of $\varphi$ in the proof system defined by $M$. Unfortunately, we can't prove that this proof system is sound (without finding an inconsistency in ZFC): if we could, then we could convert that proof into a proof that ZFC is consistent, violating Gödel's second incompleteness theorem.

Of course, if P = NP, then there is a sound and complete proof system which ignores $p$ entirely...

### This is stupid

If we now make the statement you quoted precise, it becomes: "If for every sound proof system there is a sequence $(\varphi_i)_{i\in\mathbb{N}}$ of tautologies, such that $\varphi_n$ has length $n$ for every $n$ and such that there is no polynomial $P$ such that for every $n$ $\varphi_n$ has a valid proof of length at most $P(n)$, then P $\ne$ NP."

Since we don't have a practical method for checking whether a proof system is sound, I can't help but think that this statement is completely pointless (like many tautologies).

it should not be closed. $\endgroup$ – Paul Taylor Apr 28 '15 at 7:07proofthat isshort" as "short proof" :) $\endgroup$ – user 1 Apr 28 '15 at 17:56