# On the (Cook) definition of a propositional proof system [closed]

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

A&C

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

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