Solomon Feferman

   Reductions of theories of countable tree ordinals to ID_1


This is a report of a section from the forthcoming chapter by Jeremy
Avigad and myself on Goedel's functional ("Dialectica"
interpretation.* I will sketch two applications of this
interpretation, one for a classical and one for an intuitionistic
theory of countable tree ordinals, to reduce them to corresponding
systems of one arithmetical inductive definition.  The questions
following this work are: (i) how these are related, and (ii) can
anything similar be done for theories of higher ordinal number
classes?

*To appear in the Handbook of Proof Theory, S. Buss ed.