FOM: transfinite progressions etc.

[William Tait]

At 10:53 AM -0400 7/18/02, Neil Tennant wrote:
>Could anyone please refer me to recent, state-of-the-art presentations of
>known results and open problems in the following areas:
>
>1. Transfinite recursive progressions of arithmetical theories.
>2. Ditto, but starting with HA and using only intuitionistic logic for
>closure at every stage.
>3. HA* (HA with axiom schemata of transfinite induction for recursive
>well-orderings).

Neil,

I don't understand HA*. How is it to be formalized?  Bill