×

Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel’s T and definability of ordinal numbers). (German) Zbl 0685.03038

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 [J.-Y. Girard and 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 G. Jäger and 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.
Reviewer: P.Päppinghaus

MSC:

03F10 Functionals in proof theory
03F15 Recursive ordinals and ordinal notations
03D60 Computability and recursion theory on ordinals, admissible sets, etc.
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aczel, P.: Describing ordinals using functionals of transfinite type. JSL37, 35–47 (1972) · Zbl 0264.02025 · doi:10.2307/2272543
[2] Barwise, J.: Admissible sets and structures. An approach to definability theory. Berlin Heidelberg New York: Springer 1975 · Zbl 0316.02047
[3] Buchholz, W., Schütte, K.: Ein Ordinalzahlensystem für die beweistheoretische Abgrenzung der{\(\Pi\)} 2 1 -Separation und Bar-Induktion. Bayer. Akad. Wiss. Math.-Naturwiss. Kl. Sitzungsber.1983, 99–132 (1984) · Zbl 0573.03028
[4] Feferman, S.: Ordinals associated with theories for one inductively defined set (preliminary version). Hektographiertes Manuskript eines Beitrags zur Summer Conference at Buffalo N.Y. 1968
[5] Feferman, S.: Hereditarily replete functionals over the ordinals. In: Kino, A., Myhill, J., Vesley, R.E. (eds.) Intuitionism and proof theory. Proceedings of the Summer Conference at Buffalo N.Y. 1968, pp. 289–301. Amsterdam London: North-Holland 1970 · Zbl 0218.02025
[6] Girard, J.-Y.: Functionals and ordinoids. In: Colloques internationaux du CNRS: Colloque international de logique.249, 59–71 (1975)
[7] Girard, J.-Y.: Proof theory and logical complexity, wird erscheinen in Ed. Bibliopolis, Napoli
[8] Girard, J.-Y., Ressayre, J.P.: Elements de logique{\(\Pi\)} n 1 . In: Nerode, A., Shore, R.A. (eds.) Recursion theory. Proc. Sympos. Pure Math.42, 389–445 (1985) · Zbl 0573.03029
[9] Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica12, 280–287 (1958) · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[10] Hinman, P.G.: Recursion-theoretic hierarchies. Berlin Heidelberg New York: Springer 1978 · Zbl 0371.02017
[11] Howard, W.A.: Transfinite induction and transfinite recursion. In: Stanford report on the foundations of analysis, sec. VI, Vol.2, pp. 207–262, Stanford University 1963
[12] Howard, W.A.: Hereditarily majorizable functionals of finite type. In: Troelstra, A.S.: Metamathematical investigation of intuitionistic arithmetic and analysis (Lect. Notes Math., vol. 344, pp. 454–461, Appendix) Berlin Heidelberg New York: Springer 1973
[13] Jäger, G.: Some proof-theoretic contributions to theories of sets. In: The Paris Logic Group (ed.) Logic Colloquium ’85. Proceedings of the Colloquium held in Orsay, France, July 1985, pp. 171–191. Amsterdam New York Oxford Tokyo: North-Holland 1987
[14] Jäger, G., Pohlers, W.: Eine beweistheoretische Untersuchung von ({\(\Delta\)} 2 1 CA)+(BI) und verwandter Systeme. Bayer. Akad. Wiss. Math.-Naturwiss. Kl. Sitzungsber.1982, 1–28 (1982) · Zbl 0526.03035
[15] Jensen, R.B., Karp, C: Primitive recursive set functions. In: Scott, D.S. (ed.) Axiomatic set theory. Proc. Sympos. Pure Math.,13 (I), 143–176, (1971)
[16] Päppinghaus, P.: A typed{\(\lambda\)}-calculus and Girard’s model of ptykes. In: Dorn, G., Weingartner, P. (eds.) Foundations of logic and linguistics:problems and their solutions, pp. 245–279. New York London: Plenum Press 1985
[17] Päppinghaus, P.: Ptykes in GödelsT und Verallgemeinerte Rekursion über Mengen und Ordinalzahlen. Habilitationsschrift. Universität Hannover 1985 · Zbl 0576.03035
[18] Päppinghaus, P.:{\(\Pi\)} 2-models of extensions of Kripke-Platek set theory. In: The Paris Logic Group (ed.) Logic Colloquium ’85. Proceedings of the Colloquium held in Orsay, France, July 1985, pp. 213–232. Amsterdam New York Oxford Tokyo: North-Holland 1987
[19] Päppinghaus, P.: Rekursion über Dilatoren und die Bachmann-Hierarchie. Arch. Math. Logic28, 57–73 · Zbl 0675.03033
[20] Pfeiffer, H.: Ein abstraktes Ordinalzahlbezeichnungssystem mit einem Zeichen für die kleinste schwach unerreichbare Ordinalzahl. Institut für Mathematik, Universität Hannover, Nr. 155, 1983
[21] Ressayre, J.P.: Bounding generalized recursive functions of ordinals by effective functors; a complement to the Girard theorem. In: Stern, J. (ed.) Proceedings of the Herbrand Symposium. Logic Colloquium ’81, pp. 251–279. Amsterdam New York Oxford: North-Holland 1982 · Zbl 0513.03020
[22] Richter, W., Aczel, P.: Inductive definitions and reflecting properties of admissible ordinals. In: Fenstad, J.E. Hinman, P.G. (eds.) Generalized recursion theory. Proceedings of the 1972 Oslo Symposium, pp. 301–381. Amsterdam London New York: North-Holland 1974 · Zbl 0318.02042
[23] Troelstra, A.S.: Metamathematical investigation of intuitionistic arithmetic and analysis (Lect. Notes Math., vol.344) Berlin Heidelberg New York: Springer 1973 · Zbl 0275.02025
[24] Vogel, H.: Über die mit dem Bar-Rekursor vom Typ 0 definierbaren Ordinalzahlen. Arch. Math. Logik19, 165–173 (1978) · Zbl 0414.03034 · doi:10.1007/BF02011877
[25] Weyhrauch, R.W.: Relations between some hierarchies of ordinal functions and functionals. Thesis, Stanford University 1972
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.