A Typed λ-calculus and Girard’s Model of Ptykes
In a fundamental paper inaugurating Π1/2-logic Girard (1981) introduced the notion of a dilator as a functor from the category of ordinals into itself preserving direct limits and pull-backs. In Chapter 12 of a forthcoming book (Girard (198.)) he generalizes this notion to all finite types. For every finite type σ a category PTσ is defined whose objects form a (proper) class Ptσ and are called ptykes of type σ. In annex 12.A of his book Girard proves the ptykes of finite types to be a model of a variant T’ of Gödel’s T. Using this new model he proposes an intrinsic “ordinal assignment” to terms of T’. To (closed) terms of type o → o, in particular, their value at ω is assigned. We are interested in determining these values.
KeywordsFinite Type Direct Limit Proof Theory Characteristic Term Principal Constituent
Unable to display preview. Download preview PDF.
- Barendregt, H. P., 1981, “The Lambda Calculus,” North-HoHand, Amsterdam.Google Scholar
- Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., 1981, “Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies,” Springer, Berlin.Google Scholar
- Feferman, S., 1968, “Ordinals Associated with Theories for One Inductively Defined Set,” unpublished typescript (of a lecture given at the 1968 summer conference at Buffalo, New York).Google Scholar
- Girard, J.-Y., 198., “Proof Theory and Logical Complexity,” Bibliopolis, Naples (to appear).Google Scholar
- Zucker, J. I., 1973, Iterated Inductive Definitions, Trees and Ordinals, in: Troelstra (1973, pp. 392-453).Google Scholar