What defines a "short proof"? I would like to know what the definition of a short proof is.
In Lance Fortnow’s article “The Status of the P Versus NP Problem”, Communications of the ACM, Vol. 52 No. 9, he says,

If a formula θ is not a tautology, we can give an easy proof of that fact by exhibiting an assignment of the variables that makes θ false. But if θ were indeed a tautology, we don’t expect short proofs. If one could prove there are no short proofs of tautology that would imply P ≠ NP.

I have tried to find a definition of a “short proof”, but have not been able to.
 A: 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).
A: The statement you quoted is somewhat sloppy, since there is no precise notion of a short proof for a single formula.  There is, however, a notion of short proofs for a class $C$ of formulas, when the class contains formulas of arbitrarily high length.  One says that $C$ admits short proofs if there is a polynomial $p(x)$ such that, for every natural number $n$, all formulas in $C$ of length $n$ have proofs of length at most $p(n)$.  
