A propositional proof system P p-simulates Q (written as P ≤pQ) when there is a polynomial-time function F such that P(F(x)) = Q(x) for every x. That is, given a Q-proof x, we can find in polynomial time a P-proof of the same tautology. If P ≤pQ and Q ≤pP, the proof systems P and Q are p-equivalent. There is also a weaker notion of simulation: a pps P simulates or weakly p-simulates a pps Q if there is a polynomial p such that for every Q-proof x of a tautology A, there is a P-proof y of A such that the length of y, |y| is at most p(|x|). (Some authors use the words p-simulation and simulation interchangeably for either of these two concepts, usually the latter.) A propositional proof system is called p-optimal if it p-simulates all other propositional proof systems, and it is optimal if it simulates all other pps. A propositional proof system P is polynomially bounded (also called super) if every tautology has a short (i.e., polynomial-size) P-proof. If P is polynomially bounded and Q simulates P, then Q is also polynomially bounded. The set of propositional tautologies, TAUT, is a coNP-complete set. A propositional proof system is a certificate-verifier for membership in TAUT. Existence of a polynomially bounded propositional proof system means that there is a verifier with polynomial-size certificates, i.e., TAUT is in NP. In fact these two statements are equivalent, i.e., there is a polynomially bounded propositional proof system if and only if the complexity classes NP and coNP are equal. Some equivalence classes of proof systems under simulation or p-simulation are closely related to theories of bounded arithmetic; they are essentially "non-uniform" versions of the bounded arithmetic, in the same way that circuit classes are non-uniform versions of resource-based complexity classes. "Extended Frege" systems (allowing the introduction of new variables by definition) correspond in this way to polynomially-bounded systems, for example. Where the bounded arithmetic in turn corresponds to a circuit-based complexity class, there are often similarities between the theory of proof systems and the theory of the circuit families, such as matching lower bound results and separations. For example, just as counting cannot be done by an circuit family of subexponential size, many tautologies relating to the pigeonhole principle cannot have subexponential proofs in a proof system based on bounded-depth formulas (and in particular, not by resolution-based systems, since they