6
$\begingroup$

An abstract proof system is a polynomial time function $f$ whose range is equal to the set of tautologies. If $\tau$ is a tautology, then an $f$-proof of $\tau$ is any value $\pi$ such that $f(\pi) = \tau$.

Is there an example of a propositional proof system which doesn't satisfy this definition?

$\endgroup$
  • 2
    $\begingroup$ You could take any proof system $f$ that does meet the definition and add a vacuous computation of some exponential function before the appropriate tautology is returned. $\endgroup$ – Martin Berger Dec 9 '15 at 8:48
9
$\begingroup$

Natural examples of propositional proof systems that do not fall under this definition are algebraic proof systems where the lines in the proof are arbitrary polynomials (not necessarily fully expanded). To verify the correctness of such proofs, among other things one has to test the identity of polynomials, which is not known to be possible in deterministic polynomial time.

Cf. the paper "Algebraic propositional proof systems" by Toni Pitassi, in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 31, Descriptive Complexity and Finite Models, Immerman and Kolaitis (Eds.), pp. 215-244, 1996.

$\endgroup$
2
$\begingroup$

Assume that you have an algorithm $A$ which satisfies soundness and completeness. You can define a new proof checker which is sound, complete, and runs in polynomial time: it checks if a given $\pi$ is a accepting computation history of $A$ which can be done in polynomial time (in fact $AC^0_2$).

The take away is if a proof system is not polynomial time then it is moving from a simple proof checker to something that has to compute and find (some parts of) the proof. There is a trade off between length of shortest proofs and the efficiency of the proof checker. A proof checker is not supposed to search for a proof, just check if a given proof is correct.

This is true even in the case of examples that Jan mentions in his answer. The main issue is not that they are algebraic, the main issue is that they are semantic not syntactic: the condition that one line follows from previous ones cannot be checked efficiently. These systems are mainly for mathematical understanding, not proof checking algorithms that can be used (in their semantic form).

For proof checker to make sense in practice we need it to be sound, complete, and efficient (in the general sense, not just what is implied by Cobham thesis).

$\endgroup$
  • $\begingroup$ Although Toni's system and Toni's and my recent systems are semantic, most previous algebraic proof systems are in fact syntactic and can be checked line by line (Nullstellensatz proof system, PC or Grobner system, PCR). $\endgroup$ – Joshua Grochow Dec 9 '15 at 20:36
  • $\begingroup$ @Joshua, yes, that is my point. What makes them not satisfy Cook-Reckhow conditions is not that they are algebraic but that they are semantic. $\endgroup$ – Kaveh Dec 9 '15 at 20:47
  • $\begingroup$ My point was about the syntactic algebraic systems: Nullstellensatz, PC, and PCR are syntactic, but still only have randomized verification. $\endgroup$ – Joshua Grochow Dec 9 '15 at 21:25
  • $\begingroup$ @Josh, if checking lines is randomized then you don't really have soundness for the efficient randomized proof checker algorithm anymore. I don't think it is a syntactic proof system as I meant but I admit that is arguable. $\endgroup$ – Kaveh Dec 9 '15 at 22:37
  • $\begingroup$ You can verify the lines deterministically, but if the degree is more than constant then doing so can take more than polynomial time. I thought soundness just meant that if there exists a proof, then the original statement is true; soundness doesn't depend on the complexity of the proof-checking procedure... $\endgroup$ – Joshua Grochow Dec 9 '15 at 23:04

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.