# 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.

• In fact, if "there are no short proofs of tautology" then coNP != NP. $\;$ – user5810 Apr 28 '15 at 2:23
• It's a naive question but there have been two excellent answers, so it should not be closed. – Paul Taylor Apr 28 '15 at 7:07
• One calls "A proof that is short" as "short proof" :) – user 1 Apr 28 '15 at 17:56

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)$.

• I'd like to stress that even for classes of formulas, "short proof" is not a technical term with an established definition, but a context-dependent jargon, and it may mean something else than polynomial in another situation. – Emil Jeřábek Apr 28 '15 at 10:08
• I agree with Emil. Here it is the mention of P and NP that allows us to infer that Fortnow's definition of "short" is "polynomial". – Timothy Chow Apr 28 '15 at 19:56

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).