ManuscriptsWe given an exposition of Reckhow’s theorem from his thesis, which extends Spira’s formula balancing to Frege proofs. This balancing theorem, which doesn’t appear explicitly in the thesis, is essential for showing that all Frege proofs are p-equivalent, one of the main results of the thesis.
An alternative exposition can be found in Krajíček’s monograph Bounded Arithmetic, Propositional Logic and Complexity Theory.
