On Frege and Extended Frege Proof Systems
Jan Krajı́ček · Birkhäuser Boston eBooks · 1995
We propose a framework for proving lower bounds to the size of EF -proofs (equivalently, to the number of proof-steps in F -proofs) in terms of boolean valuations . The concept is motivated by properties of propositional provability in models of bounded arithmetic and it is a finitisation of a particular forcing construction explained also in the paper. It reduces the question of proving a lower bound to the question of constructing a partial boolean algebra and a map of formulas into that algebra with particular properties. We show that in principle one can obtain via this method optimal lower bounds (up to a polynomial increase).