A non-well-founded primitive recursive tree provably well-founded for co-r.e. sets

 We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ₁ ⁰. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ₁ ⁰, equals the limit of all recursive ordinals ω₁ ^ck . RID="ID=" <E5>Mathematics Subject Classification (2000):&ensp;03B30</E5>, 03F15 RID="ID=" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium f&uuml;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 &ndash; 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&Ouml;LLERFELD for remarks on a previous title. Received: 27 July 2000 / Published online: 25 February 2002 RID=" ID=" <E5>Mathematics Subject Classification (2000):&ensp;03B30</E5>, 03F15 RID=" ID=" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium f&uuml;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 &ndash; 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&Ouml;LLERFELD for remarks on a previous title.