Pseudo-Hierarchies in Admissible Set Theory without Foundation and Explicit Mathematics Inauguraldissertation der Philosophisch-naturwissenschaftlichen Fakulta(cid:127)t der Universita(cid:127)t Bern vorgelegt von Dieter Probst von Langnau i. E. Leiter der Arbeit: Prof. Dr. G. Ja(cid:127)ger Institut fu(cid:127)r Informatik und angewandte Mathematik Contents Introduction 1 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 I Languages, theories and provable ordinals 9 I.1 General conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 I.1.1 Mathematical reasoning and formal proofs . . . . . . . . . . . 9 I.1.2 Notational conventions . . . . . . . . . . . . . . . . . . . . . . 10 I.1.3 Sets, functions and relations . . . . . . . . . . . . . . . . . . . 10 I.1.4 Orderings, trees and ordinals . . . . . . . . . . . . . . . . . . . 11 I.1.5 Recursive and primitive recursive functions and relations . . . 13 I.1.6 Some primitive recursive functions and relations . . . . . . . . 14 I.1.7 Indices for the [primitive] recursive functions and relations . . 15 I.2 Languages, theories and structures . . . . . . . . . . . . . . . . . . . 16 I.2.1 Languages, theories and structures . . . . . . . . . . . . . . . 16 I.2.2 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 I.2.3 The languages L and L of (cid:12)rst and second order arithmetic . 20 1 2 I.2.4 The language L(cid:3) of Kripke-Platek set theory . . . . . . . . . . 21 I.2.5 The language L for explicit mathematics . . . . . . . . . . . . 22 I.2.6 First and second order predicate logic and the logic of partial terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 I.2.7 Peano Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . 24 I.2.8 The semi-formal systems PA(cid:3) . . . . . . . . . . . . . . . . . . 25 I.2.9 The theories BS0 and KPu0 . . . . . . . . . . . . . . . . . . . 26 I.2.10 ACA and ACA : Second order theories with arithmetical com- 0 prehension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 I.2.11 The theory EETJ . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 I.2.12 Translations and embeddings . . . . . . . . . . . . . . . . . . 32 I.2.13 On the dispensability of primitive recursive function symbols . 34 I.2.14 Syntactical extensions of L . . . . . . . . . . . . . . . . . . . 35 2 I.3 Proof-theoretic basics . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 I.3.1 A notation system based on the ternary Veblen function . . . 36 iii iv Contents I.3.2 Cut-Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 37 I.3.3 The proof-theoretic ordinal jTj of a theory T . . . . . . . . . . 40 II Pseudo-hierarchies in second order arithmetic 43 II.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 II.1.1 Universal formulas . . . . . . . . . . . . . . . . . . . . . . . . 44 II.1.2 Trees and normal forms of (cid:5)1 and (cid:6)1 formulas of L . . . . . . 46 1 1 2 II.1.3 Hierarchies and choice sequences . . . . . . . . . . . . . . . . 52 II.1.4 N-models of (cid:6)1-AC and (cid:6)1-DC . . . . . . . . . . . . . . . . . . 54 1 1 II.1.5 The jump-hierarchy . . . . . . . . . . . . . . . . . . . . . . . . 58 II.1.6 The hyper-arithmetical sets HYP . . . . . . . . . . . . . . . . 62 II.2 Pseudo-hierarchy arguments . . . . . . . . . . . . . . . . . . . . . . . 66 II.2.1 On HYP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 II.2.2 The theory ACA +((cid:1)-TR) . . . . . . . . . . . . . . . . . . . 76 0 II.2.3 Fixed points of monotone and non-monotone operators . . . . 78 II.2.4 Fixed points and hyperarithmetical sets . . . . . . . . . . . . 81 II.2.5 The proof-theoretic analysis of FP(cid:0) . . . . . . . . . . . . . . . 87 0 II.2.6 Additional results on the class FixA . . . . . . . . . . . . . . . 90 IIIPseudo-hierarchy arguments in admissible set theory without foun- dation and explicit mathematics 95 III.1 Pseudo-hierarchies in admissible set theory . . . . . . . . . . . . . . . 96 III.1.1 Hierarchies and pseudo-hierarchies . . . . . . . . . . . . . . . 96 III.1.2 Admissible sets and the theories KPi0, KPir and KPm0 . . . . . 97 III.1.3 A pseudo-hierarchy principle for KPi0 . . . . . . . . . . . . . . 100 III.1.4 Extending theories by (psh0) . . . . . . . . . . . . . . . . . . . 101 III.1.5 Fixed point principles vs. iteration principles . . . . . . . . . . 105 III.1.6 On linearity, iteration and choice . . . . . . . . . . . . . . . . 110 III.2 Admissible sets and linearity . . . . . . . . . . . . . . . . . . . . . . . 111 III.2.1 The constructible hierarchy L . . . . . . . . . . . . . . . . . . 112 III.2.2 A (cid:1) formula expressing admissibility . . . . . . . . . . . . . . 115 0 III.2.3 On hyp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 III.2.4 Admissibles linearly ordered by 2 . . . . . . . . . . . . . . . . 127 III.2.5 Dependent choice in admissible set theory . . . . . . . . . . . 129 III.3 Pseudo-hierarchies in explicit mathematics . . . . . . . . . . . . . . . 140 III.3.1 Hierarchies and pseudo-hierarchies . . . . . . . . . . . . . . . 140 III.3.2 The theory EMA . . . . . . . . . . . . . . . . . . . . . . . . . 142 0 III.3.3 A pseudo-hierarchy principle for EMA . . . . . . . . . . . . . 143 0 III.3.4 Choice in explicit mathematics . . . . . . . . . . . . . . . . . 148 III.3.5 EMA , OMA and asymmetric interpretations . . . . . . . . . . 149 0 Contents v Index 161 Introduction Pseudo-hierarchies have become a powerful tool in several areas of mathematical logic. They were (cid:12)rst applied in the context of hyperarithmetical theory by Spec- tor [41], Gandy [16] and Feferman and Spector [13]. Especially in second order arithmetic, the potent and (cid:13)exible technique of pseudo-hierarchy arguments seems nowadays virtually indispensable. A typical application for speci(cid:12)c (cid:12)xed point def- initions is given in Avigad [2], and a rich fund of important results obtained by working with pseudo-hierarchies, e.g. the pairwise equivalence of (ATR), the Perfect Set Theorem and (cid:6)0 determinacy, can be found in Simpson [40]. Without even 1 looking at the many more instances of pseudo-hierarchy arguments for second order arithmetic gathered in [40] and the second chapter of this thesis, it is not presump- tuous to wish for an equally potent device in subsystems of set theory or explicit mathematics. Making the uncon(cid:12)ned application of pseudo-hierarchy arguments possible in sub- systems of admissible set theory without foundation and explicit mathematics has been the leading goal of this thesis. After a careful analysis of pseudo-hierarchies is second order arithmetic, (cid:12)rstly to understand this method thoroughly with regard to its subsequent adaption to the aforementioned frameworks, and secondly to em- phasis the versatility of this technique by applying it in order to achieve own results, we pinpoint the obstacles on the road to success and provide e(cid:11)ective strategies to sidestep these di(cid:14)culties. Besides, we research various (cid:12)xed point theories: Among otherthings,weprovethatoperationsinducedbypositivearithmeticalformulaspos- sess ingeneralno(cid:1)1 de(cid:12)nable (cid:12)xed points, althoughthere arewell-know methodsto 1 obtain (cid:6)1 as well as (cid:5)1 de(cid:12)nable (cid:12)xed points (see e.g. [1]). As a nice by-product of 1 1 thislineofresearch, weobtainanembedding ofID(cid:3) (thetheoryobtainedfromID by 1 1 restricting (cid:12)xed point induction to formulas that contain (cid:12)xed point constants only positively) into (cid:6)1-DC, and thereby answer an old question ask in Feferman’s article 1 on Hancock’s conjecture [11] about the upper bound of ID(cid:3). Claiming (cid:12)xed points 1 of monotone, (cid:6) de(cid:12)nable operations on the entire universe over KPi0 leads to the theory KPi0 +((cid:6)-fp0) with the same proof-theoretic ordinal as KPm0, the standard theory of strength meta-predicative Mahlo in admissible set theory (cf. Ja(cid:127)ger and Strahm [27]). This result depends crucially on the application of pseudo-hierarchy 1 2 Introduction arguments. Further, we study a strengthening of KPi0 (cf. Ja(cid:127)ger [19]) where not only the admissibles distinguished by the predicate Ad(x) are linearly ordered by 2, but all sets re(cid:13)ecting the Kripke-Platek axioms. Surprisingly, this extension has already the strength of (cid:1)1-CA . Moreover, we elaborate on the connection between 2 0 iteration and dependent choice: We demonstrate how the axiom of KPm0 asserting that the class fx : Ad(x)g is linearly ordered by 2 is used to embed trans(cid:12)nite de- pendent choice, and that this axiom can be compensated by claiming (cid:5) re(cid:13)ection 2 on admissibles that additionally satisfy dependent choice, which nicely parallels the situation in second order arithmetic where extending ACA by (cid:5)1-re(cid:13)ection on mod- 0 2 els of (cid:6)1-DC leads also to a theory of strength meta-predicative Mahlo (cf. Ru(cid:127)ede 1 [37],[38]). Finally, we propose a form of dependent choice suitable for subsystems of explicit mathematics. The concept of a hierarchy is based on the notion of an operation: In second order arithmetic, a formula A(U;u) induces canonically an operation FA acting on the powerset of the natural numbers and mapping X to fx : A(X;x)g. By iterating such an operation along a well-ordering (cid:30), a proper hierarchy G is obtained whose (cid:11)th level (G) := FA((G) ) is the FA image of the disjoint union of the levels (cid:11) (cid:30)(cid:11) (G) below (cid:11). Proper hierarchies on their own constitute a very powerful and (cid:12) useful concept which is implemented in Friedman’s well-known theory ATR (cf. e.g. 0 Friedman [14], Friedman/McAloon/Simpson[15], Steel [42]) and, at least in second order arithmetic, are intrinsically tied to pseudo-hierarchies. A pseudo-hierarchy looks locally like a proper hierarchy, so again (G) = FA((G) ), however, the (cid:11) (cid:30)(cid:11) underlying ordering (cid:30) is only a linear ordering but not well-founded. In subsystems of second order arithmetic comprising arithmetical comprehension, the existence of a pseudo-hierarchy for A follows already if FA can be iterated along arbitrary well-orderings. Moreover, such a pseudo-hierarchy can inherit a chosen (cid:6)1 1 de(cid:12)nable property ofthe proper hierarchy: If A(U;u)is anarithmetical and B(U;V) a (cid:6)1 formula of second order arithmetic such that 1 8X[Wo(X) ! 9F(HierA(F;X)^B(F;X))]; then the well-known fact that being a well-ordering cannot be expressed by a (cid:6)1 1 formula forces the existence of a linear ordering (cid:30) that is not a well-ordering and a hierarchy G that meet HierA(G;(cid:30))^B(G;(cid:30)). Each pseudo-hierarchy argument exploits that the (cid:12)eld of the underlying ordering (cid:30) of the pseudo-hierarchy possesses a set K (cid:18) Field((cid:30)) that is open at the bottom, i.e. K is non-empty, upward closed and has no (cid:30)-least element. To apply its simplest form, we consider a pseudo-jumphierarchy G along the linear ordering (cid:30). Basically, (G) is the collection of all sets that are (cid:5)0 in some level (G) for (cid:13) (cid:30) (cid:11). Then, for (cid:11) 1 (cid:13) a set K open at the bottom, the collection M of all sets that are contained in each Introduction 3 level (G) for (cid:11) 2 K is closed under arithmetical comprehension: If the set X is (cid:11) arithmetical in some set Y 2_ M, then X is already (cid:5)0 in Y for some n 2 N. Given n a (cid:12)xed but arbitrary (cid:11) 2 K, there is a sequence (cid:11) (cid:31) (cid:11) (cid:31) ::: (cid:31) (cid:11) of elements of 0 0 1 n K. Since Y is also in (G) , the de(cid:12)nition of the jumphierarchy yields that X is an (cid:11)n element of (G) . Hence, the set X is in each (G) for (cid:13) 2 K, thus also in M. (cid:11)0 (cid:13) Often, one can boost the above argument by imposing additional properties on the pseudo-hierarchy. Avigad’s argument in [2] for instance, considers a monotone op- eration FA induced by an arithmetical formula. Then, there is a monotone pseudo- hierarchy G where (G) = FA( (G) ) and further, if x 2 (G) , then there is (cid:11) (cid:12)(cid:30)(cid:11) (cid:12) (cid:11) a (cid:30)-least level (cid:11) where x appears (cid:12)rst. For a set K open at the bottom, each 0 S x 2 Z := (G) enters the hierarchy at a least level (cid:11) . Clearly, (cid:11) is not in K, (cid:11)2K (cid:11) 0 0 otherwise there is a (cid:12) 2 K with (cid:12) (cid:30) (cid:11) , contradicting that x 2 Z. Therefore, each 0 T x 2 Z enters the hierarchy already at some level below K, thus Z = (G) . (cid:11)(cid:30)K (cid:11) Regarding Z as a union, the monotonicity of the operation and the hierarchy imply S that (G) (cid:18) FA(Z) for all (cid:11) (cid:30) K, whereas regarding Z as an intersection yields (cid:11) FA(Z) (cid:18) (G) for all (cid:11) 2 K, thus FA(Z) = Z. (cid:11) A more general form of the condition imposed on the pseudo-hierarchy above is to stipulate that the underlying ordering (cid:30) of a pseudo-hierarchy G, which is not a well-ordering, looks like a well-ordering in a model D of ACA above G. If G is a pseudo-jumphierarchy conform with this condition, then the collection M from our (cid:12)rst example is even a model of (cid:6)1-AC: If 8x9XA(X;x) holds in M for some 1 arithmetical formula A(U;u), then f(cid:11) 2 Field((cid:30)) : 8x(9X 2_ (G) )A(X;x)g (cid:11) is a superset of K in D. Therefore it has a least element (cid:11) , which is already below 0 K. Hence, Y := (G) 2_ M, and for each x there is a least index e such that (cid:11)0 x A((Y) ;x). Applying arithmetical comprehension in M yields a set Z 2_ M with ex (Z) = Y , thus 8xA((Z) ;x). The property that the underlying ordering (cid:30) of a x ex x pseudo-hierarchy G lookslike a well-ordering in a model D ofACA above G is indeed so apt for pseudo-hierarchy arguments that we hardly ever need supplementary conditions. Our declared aim is to establish an analogue situation with respect to pseudo- hierarchies in subsystems of admissible set theory without foundation and explicit mathematics. In admissible set theory, for instance, there exist initial segments of the constructible hierarchy L along arbitrary well-orderings, so we ask for a con- structible hierarchy along a linear ordering that is not wellfounded. Obviously, this wish is not to ful(cid:12)ll in a well-founded universe, which highlights that the existence of pseudo-hierarchies is not provable without additional assumptions. In particular, neither in admissible set theory nor in explicit mathematics one can disprove that 4 Introduction being a well-ordering is expressible by a (cid:6) or a (cid:6)+ formula, respectively, which un- dermines the argument applied in second order arithmetic to prove the existence of pseudo-hierarchies and forces us to come up with new ideas. In accordance with the setting in second order arithmetic, we base the concept of a hierarchy in admissible set theory upon the notion of an operation: A formula A(u;v) induces an operation fA, if for each set x there exists exactly one set y such that A(x;y). The set y is then denoted by fA(x). When iterating an operation fA along a well-ordering (cid:30), we obtain a proper hierarchy, namely a function g with domain Field((cid:30)) where g((cid:11)) = fA(g(cid:22)(cid:11)) for each (cid:11) in the domain of g. Again, a pseudo-hierarchy g looks locally like a proper hierarchy but its domain is a linear ordering that is not well-founded. Motivated by the previous example and assured by experience, we settle for the following pseudo-hierarchy principle: For all (cid:6) operations fA, such that 8x[Wo(x) ! 9ghierA(g;x)]; there exists a linear ordering (cid:30) that is not a well-ordering and a hierarchy g that meet hierA(g;(cid:30))^Wog+((cid:30)), where g+ denotes the least admissible above g. This principle is not provable in a normal theory T of admissible sets, however, the following strategy o(cid:11)ers an excellent workaround: We simply extend T by the above pseudo-hierarchy principle. Provided that jTj < j(cid:5)1-CA j, then this extension 1 0 is consistent, and moreover, has still the same proof-theoretic ordinal. Namely, if we can iterate a (cid:6) operation fA along arbitrary well-orderings but no pseudo- hierarchy forfA exists, then 8x[Wo(x) $ 9g(HierfA(g;x)^Wog+(x)]. Exploiting the universal character of the formula Wo(x) and applying (cid:1) separation then proves the translation of each instance of ((cid:5)1-CA) and thus also each ordinal (cid:11) below j(cid:5)1-CA j, 1 1 0 in particular TI (U;(cid:11)). Consequently, the pseudo-hierarchy principle is derivable in (cid:1) Ty, the extension of T by the axiom :TI (U;jTj), stating that the relation U does (cid:1) not have a least element with respect to the underlying ordering (cid:1) of our notation system. Finally, jTj = jTyj is a consequence of an extension of Schu(cid:127)tte’s famous boundedness Theorem (cf. [39]) shown in Ja(cid:127)ger and Probst [25] and summarized in subsection III.1.4. In explicit mathematics, the setting is again slightly di(cid:11)erent, and additional prob- lems have tobe dealt with. The canonic notion ofan operationspecifying the transi- tion from one level of a hierarchy to the next is now an individual term (f : < ! <) thatmapsnamestonames. Alsoahierarchyfortheoperationf alongtheordering(cid:30) is represented by an individual term (h : Field((cid:30)) ! <) that assigns names of types tothe elements ofthe(cid:12)eld of(cid:30) insuch away thath((cid:11)) = f(j(f(cid:12) : (cid:12) (cid:30) (cid:11)g;h)). Now the statement that h is a hierarchy for the operation f along the ordering (cid:30) is a (cid:6)+ formula, a (cid:6) formula that contains the naming predicate < only positively. Unfor- tunately, the lack of an appropriate form of (cid:1) separation prevents to infer ((cid:5)1-CA) 1