An inside view of EXP or The closed fragment of the provability logic of ΙΔo+Ω₁ with a propositional constant for EXP

Abstract

We characterize the closed fragment of the provability logic of ΙΔo+EXP with a propositional constant for EXP. In three appendices the details of various results in Arithmetic needed for our characterization are provided