A Typed λ-calculus and Girard’s Model of Ptykes

  • Peter Päppinghaus


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.


Finite Type Direct Limit Proof Theory Characteristic Term Principal Constituent 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Barendregt, H. P., 1981, “The Lambda Calculus,” North-HoHand, Amsterdam.Google Scholar
  2. 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
  3. 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
  4. Girard, J.-Y., 1981, π1/2-Logic, Part 1: Dilators, Annals of Math. Logic, 21:75–219.CrossRefGoogle Scholar
  5. Girard, J.-Y., 198., “Proof Theory and Logical Complexity,” Bibliopolis, Naples (to appear).Google Scholar
  6. Troelstra, A. S., 1973, “Metaraathematical Investigation of Intuitionistic Arithmetic and Analysis,” Springer, Berlin.CrossRefGoogle Scholar
  7. Zucker, J. I., 1973, Iterated Inductive Definitions, Trees and Ordinals, in: Troelstra (1973, pp. 392-453).Google Scholar

Copyright information

© Springer Science+Business Media New York 1985

Authors and Affiliations

  • Peter Päppinghaus
    • 1
  1. 1.Institut für MathematikUniversität HannoverHannoverGermany

Personalised recommendations