Simpson showed that ATR0 can interpret, using well-founded trees modulo bisimulation, a weak fragment of set theory without the powerset axiom. The interpretation via well-founded trees is quite versatile and can be used in systems outside that of second order arithmetic. 

 

The tree interpretation can be used to interpret a fragment of set theory with n iterations of the powerset of ω in n + 2 order arithmetic. More generally, the tree interpretation can be used in fragments of set theory with restricted comprehension and α iterations of the powerset. We show that the tree interpretation, combined with the construction of the constructible universe, is sufficient to interpret a theory with collection and the same number of powersets. Furthermore, we show that the case in which α has countable cofinality is very similar to the case in which α = 0. This similarity is due to the fact that, for α of countable cofinality, an analogue of the Kleene normal form holds for the structure (Vα,Vα+1).

 

We also present conservativity results between the various systems we introduce, along with some limits to the tree interpretation. We also show that there is a variation of the tree interpration which can be carried out in weaker systems such as ACA0. Finally, we discuss the non solidity of these theories.