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

I'm a bit confused. To be a proof system every tautology needs to be able to be proven in polynomial-time?

What about proofs that a single formula follows from a set of formulas--do these proofs need to be done in polynomial-time? Such as proving: A&B-premise B&C-premise


(I'm aware one could put these three formulas into one formula and try to prove that. But technically that would be proving a single tautology and not that such and such follows from such and such.)

What I'm asking is: If one is given something like the above, but the system is such that it cannot prove A&C from the premises (in polynomial time)...yet the system can prove single formulas to be tautologies in polynomial time...then does the system meet the definition?

(let's say that in the system, for whatever reason, one can't just connect A&B, B&C, A&C in a single formula (A&B) & (B&C) --> (A&C))


closed as off-topic by Kaveh, R B, David Eppstein, Mohammad Al-Turkistany, Joshua Grochow Dec 16 '15 at 4:43

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Questions must demonstrate a minimal understanding of the problem being solved. Tell us what you've tried to do, why it didn't work, and how it should work. See also our question checklist." – Kaveh, R B, David Eppstein, Mohammad Al-Turkistany, Joshua Grochow
If this question can be reworded to fit the rules in the help center, please edit the question.


$f$ is not a prover, it's a proof-checker. $w$ is the proof. And the polynomial is a polynomial of the length of the proof, which could be much larger than the length of the thing being proved. If you have a proof system for which checking whether something really is a proof (or figuring out what it's a proof of) takes more than polynomial time, then your proofs are too gappy.


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