Truth definitions without exponentiation and the Σ1 collection scheme

We prove that: if there is a model of I△o + ≠exp with cofinal Σ1 -definable elements and a Σ1 truth definition for Σ1 sentences, then I△o + ≠ exp +≠BΣ1 is consistent, • there is a model of I △o + Ωi + ≠ exp with cofinal Σ1 -definable elements, both a Σ2 and a Σn truth definition for Σn sentences, and for each n ≥ 2, a I, truth definition for Σ n sentences. The latter result is obtained by constructing a model with a recursive truth-preserving translation of Σt sentences into boolean combinations of 3Σ 0 sentences. We also present an old but previously unpublished proof of the consistency of I△o + ≠ exp +≠BΣt under the assumption that the size parameter in Lessan's △ 0 universal formula is optimal. We then discuss a possible reason why proving the consistency of I△o + ≠ exp +≠BΣ1 unconditionally has turned out to be so difficult. © 2012. Association for Symbolic Logic.