1 results
TRANSFINITE RECURSION IN HIGHER REVERSE MATHEMATICS
-
- Journal:
- The Journal of Symbolic Logic / Volume 80 / Issue 3 / September 2015
- Published online by Cambridge University Press:
- 22 July 2015, pp. 940-969
- Print publication:
- September 2015
-
- Article
- Export citation
-
In this paper we investigate the reverse mathematics of higher-order analogues of the theory
$$ATR_0$$ within the framework of higher order reverse mathematics developed by Kohlenbach [11]. We define a theory 
$$RCA_0^3$$, a close higher-type analogue of the classical base theory 
$$RCA_0$$ which is essentially a conservative subtheory of Kohlenbach’s base theory 
$$RCA_{\rm{0}}^\omega$$. Working over 
$$RCA_0^3$$, we study higher-type analogues of statements classically equivalent to 
$$ATR_0$$, including open and clopen determinacy, and examine the extent to which 
$$ATR_0$$ remains robust at higher types. Our main result is the separation of open and clopen determinacy for reals, using a variant of Steel’s tagged tree forcing; in the presentation of this result, we develop a new, more flexible framework for Steel-type forcing.
