Comments on Beckmann's Uniform Reducts

S Cook - arXiv preprint cs/0601086, 2006 - arxiv.org
arXiv preprint cs/0601086, 2006arxiv.org
Arnold Beckmann defined the uniform reduct of a propositional proof system f to be the set of
those bounded arithmetical formulas whose propositional translations have polynomial size
f-proofs. We prove that the uniform reduct of f+ Extended Frege consists of all true bounded
arithmetical formulas iff f+ Extended Frege simulates every proof system.
Arnold Beckmann defined the uniform reduct of a propositional proof system f to be the set of those bounded arithmetical formulas whose propositional translations have polynomial size f-proofs. We prove that the uniform reduct of f + Extended Frege consists of all true bounded arithmetical formulas iff f + Extended Frege simulates every proof system.
arxiv.org