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.

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

  • 9
    $\begingroup$ 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. $\endgroup$ – Emil Jeřábek Apr 28 '15 at 10:08
  • 1
    $\begingroup$ 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". $\endgroup$ – 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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.