7
$\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$
1
  • 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$ Dec 9, 2015 at 8:48

2 Answers 2

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$
7
  • 1
    $\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$ Dec 9, 2015 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, 2015 at 20:47
  • 1
    $\begingroup$ My point was about the syntactic algebraic systems: Nullstellensatz, PC, and PCR are syntactic, but still only have randomized verification. $\endgroup$ Dec 9, 2015 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, 2015 at 22:37
  • 1
    $\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$ Dec 9, 2015 at 23:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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