Interpreting reflexive theories in finitely many axioms

Abstract

For finitely axiomatized sequential theories F and reflexive theories R, we give a characterization of the relation ‘F interprets R’ in terms of provability of restricted consistency statements on cuts. This characterization is used in a proof that the set of IIl (as well as Σl) sentences π s.t. GB interprets ZF + π is Σ0/3-complete.