Foundations of Logic and Linguistics pp 245-279 | Cite as

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

## Abstract

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.

## Keywords

Finite Type Direct Limit Proof Theory Characteristic Term Principal Constituent## Preview

Unable to display preview. Download preview PDF.

## References

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