<p>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. </p>

<p>Cf. the paper "<a href="https://www.cs.toronto.edu/~toni/Papers/pitassi-algebraic.ps">Algebraic propositional proof systems</a>" 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.  </p>

CC BY-SA 3.0
2015-12-09T09:16:56.087Z
2015-12-09T09:16:56.087Z
Jan Johannsen
<p>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$).</p>

<p>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.</p>

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

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

CC BY-SA 3.0
2015-12-09T20:36:09.700Z
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).
Joshua Grochow
CC BY-SA 3.0
2015-12-09T20:47:31.277Z
@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.
Kaveh
CC BY-SA 3.0
2015-12-09T21:25:25.903Z
My point was about the syntactic algebraic systems: Nullstellensatz, PC, and PCR are syntactic, but still only have randomized verification.
Joshua Grochow
CC BY-SA 3.0
2015-12-09T22:37:01.840Z
@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.
Kaveh
CC BY-SA 3.0
2015-12-09T23:04:16.353Z
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...
Joshua Grochow
CC BY-SA 3.0
2015-12-09T23:53:45.307Z
@Josh, it does not depend on the complexity of the algorithm but it depends on the algorithm. if the verification algorithm is randomized then there is a small probability that it might accept an incorrect proof or might not accept a correct one, and if we require accepting a $\pi$ only when the probability of accepting by algorithm is at least something then it is not syntactic anymore. (But one can argue that small probability of making a mistake is fine.)
Kaveh
CC BY-SA 3.0
2015-12-10T03:28:13.923Z
Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/32772/discussion-between-joshua-grochow-and-kaveh).
Joshua Grochow
CC BY-SA 3.0
2015-12-09T11:39:04.957Z
2015-12-09T11:49:22.367Z
2015-12-09T11:49:22.367Z
Kaveh
<blockquote>
  <p>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$.</p>
</blockquote>

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

CC BY-SA 3.0
2015-12-09T08:48:00.887Z
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.
Martin Berger
<cc.complexity-theory><lo.logic><computability><proof-complexity>
Are there any propositional proof systems which are not Cook-Reckhow proof systems?
Slacked
# Are there any propositional proof systems which are not Cook-Reckhow proof systems?

(Asked by: username_0 on 2015-12-09)

> 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?

**Tags:** cc.complexity-theory, lo.logic, computability, proof-complexity
> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2015-12-09. Score: 9

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](https://www.cs.toronto.edu/~toni/Papers/pitassi-algebraic.ps)" 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.


---

### Answer by username_3 on 2015-12-09. Score: 2

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

> **Comments:**
> **username_4**: 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).  
> **username_3**: @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.  
> **username_4**: My point was about the syntactic algebraic systems: Nullstellensatz, PC, and PCR are syntactic, but still only have randomized verification.  
> **username_3**: @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.  
> **username_4**: 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...  
> **username_3**: @Josh, it does not depend on the complexity of the algorithm but it depends on the algorithm. if the verification algorithm is randomized then there is a small probability that it might accept an incorrect proof or might not accept a correct one, and if we require accepting a $\pi$ only when the probability of accepting by algorithm is at least something then it is not syntactic anymore. (But one can argue that small probability of making a mistake is fine.)  
> **username_4**: Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/32772/discussion-between-joshua-grochow-and-kaveh).  

---

