Abstract

We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ1 0. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ1 0, equals the limit of all recursive ordinals ω1 ck . RID=""ID="" Mathematics Subject Classification (2000): 03B30, 03F15 RID=""ID="" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium für Bildung, Wissenschaft, Forschung und Technologie. RID=""ID="" I would like to thank A. SETZER for his hospitality during my stay in Uppsala in December 1998 – these investigations are inspired by a discussion with him; S. BUSS for his hospitality during my stay at UCSD and for valuable remarks on a previous version of this paper; and M. MÖLLERFELD for remarks on a previous title