Translating IΔ0 + exp Proofs into Weaker Systems
Chris Pollett · Mathematical logic quarterly · 2000
The purpose of this paper is to explore the relationship between IΔ0 + exp and its weaker subtheories. We give a method of translating certain classes of IΔ0 + exp proofs into weaker systems of arithmetic such as Buss' systems S2. We show if IEi (exp) ⊢ A with a proof P of expind-rank(P) ≤ n + 1where all (∀ ≤: right) or (∃ ≤: left) have bounding terms not containing function symbols, then Si 2 ⊇ IEi,2 ⊢ An. Here A is not necessarily a bounded formula. For IOpen(exp) we prove a similar result. Using our translations we show IOpen(exp) ⊊ IΔ0(exp). Here IΔ0(exp) is a conservative extension of IΔ0 + exp obtained by adding to IΔ0 a symbol for 2 x to the language as well as defining axioms for it.