On Frege and Extended Frege Proof Systems

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.