Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers) (Q1825868): Difference between revisions

In this paper two of the inequalities are proved which are needed to obtain a result on the ordinal values of ptykes of type 2, which are definable in Gödel's T. The paper is written in German, but contains an extensive survey in English. Ptykes have been introduced by Girard as a generalization of dilators to (finite) higher types. Gödel's T is an equational calculus containing as axioms the defining equations of Gödel's primitive recursive functionals of finite types. Girard has used the ptykes of finite types to construct a natural model of a subsystem resp. variant of T and suggests to obtain from this model the following intrinsic ordinal assignment to closed T-terms of pure types. The pure types are defined inductively by \(n+1:=n\to o\). ``The'' ptyx \(\Xi_ n\) is defined to be the sum of all recursive ptykes of type n in an arbitrary enumeration. For a closed T-term of type \(n+1\) the ordinal assigned to t is \(o(t):=t(\Xi_ n).\) The main result of this paper yields the least upper bounds of \(Spec_ 1\) and of \(Spec_ 2\), where the spectra of T are defined as follows. For \(n\geq 1:\) \[ Spec_ n:=\{t(\Xi_{n-1})|\text{ t closed T-term of type }n\}. \] Rough upper bounds for these spectra follow from work of Girard and Ressayre, who study the ptykes \(\Xi_ n\) and their relation to analytic complexity [\textit{J.-Y. Girard} and \textit{J. P. Ressayre}, Recursion theory, Proc. Symp. Pure Math. 42, 389-445 (1985; Zbl 0573.03029)]. In particular they show that \(\Xi_{n+1}(\Xi_ n)\)- the supremum of the ordinals which can be described recursively in \(\Xi_ n\) as a parameter - equals the supremum of the \(\Pi^ 1_{n+1}\)-definable well-orderings of subsets of \(\omega\). The supremum of \(Spec_ 1\) is \(\Phi_{\epsilon_{\Omega +1}}(0)\), the so-called Bachmann-Howard ordinal. This ordinal also equals the supremum of the ordinals which are provably \(\Sigma_ 1\)-definable in KPu, Kripke-Platek set theory extended by an axiom of infinity. The supremum of \(Spec_ 2\) is the ordinal corresponding to the Bachmann- Howard ordinal if one builds a Bachmann hierarchy of length \(\epsilon_{\Omega +1}\) on the normal function which enumerates the topological closure of the set of countable admissible ordinals. This ordinal also equals \(\Theta^ 1_{\epsilon_{I+1}}0\), the supremum of the ordinals which are provably \(\Sigma_ 1\)-definable in KPi, Kripke- Platek set theory extended by an axiom of inaccessibility [see \textit{G. Jäger} and \textit{W. Pohlers}, Sitzungsber., Bayer. Akad. Wiss., Math.- Naturwiss. Kl. 1982, 1-28 (1982; Zbl 0526.03035)]. The main result follows from calculating uniformly for a large class of dilators G the supremum of \[ Spec(G):=\{A(G)| \quad A\in Pt^ 2,\text{ A definable in }T\}. \] This supremum is obtained by proving a chain of four inequalities. The two of these establishing an upper and a lower bound for Spec(G) are shown in this paper. The remaining inequalities are shown in earlier papers by the author [Logic Colloq. '85, Proc. Colloq., Orsay/France 1985, Stud. Logic Found. Math. 122, 213- 232 (1987; Zbl 0625.03039); Arch. Math. Logic 28, 57-73 (1989)]. The upper bound comes from a formal interpretation of an extension \(T'(G)\) of Gödel's T in an extension KP(G) of Kripke-Platek set theory without urelements. Moreover \(\Phi^ g_{\epsilon_{\Omega +1}}(0)\) is proved to be a lower bound for Spec(G) by showing a cofinal subset of \(\Phi^ g_{\epsilon_{\Omega +1}}(0)\) to be definable in \(T'(G)\), where \((\Phi^ g_{\alpha})_{\alpha <\epsilon_{\Omega +1}}\) is the Bachmann hierarchy over \(\Phi^ g_ 0=\lambda x.g^{1+x}(0)\), and g is the ordinal function induced by the dilator G.