Comments on Beckmann's Uniform Reducts

TL;DR

This paper investigates the relationship between the uniform reduct of certain proof systems and their ability to simulate all proof systems, revealing a deep connection with the strength of Extended Frege systems.

Contribution

It proves that the uniform reduct of f + Extended Frege encompasses all true bounded arithmetical formulas if and only if f + Extended Frege can simulate every proof system.

Findings

Uniform reduct of f + Extended Frege equals all true bounded arithmetical formulas

f + Extended Frege's ability to simulate all proof systems is characterized by its uniform reduct

The result links proof system strength with the scope of its uniform reduct

Abstract

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.