Proof-theory and logical complexity II

Chapters 8-12, manuscript, 1982.

This second part expounds the theory of dilators and related topics, e.g., β-proofs. The book (written in 1982) was originally intended as a whole; Per Martin-Löf convinced me to split it. The sole chapters 1-7 were published in 1987. Several changes occurred on the side of the publisher which delayed the handling of part II. On my side, I had lost faith in infinitary logic and made no effort to proofread the crude LaTeX file of chapters 8-12. I issue the document as it is, poorly formated, e.g., with the arrows missing in diagrams. Although I think that the general orientation is wrong, it contains many ideas that can perhaps be reused in another context.

Typically, the idea of a functor preserving direct limits and pullbacks, the leitmotiv of this part II, was reused to develop my own denotational semantics, coherent spaces, which would eventually lead to linear logic.

The original idea was to give a more satisfactory meaning to ordinal notations, the Cantor Normal Form and its various generalisations. The basic remark is that the replacement of the ordinal ω with the integer n in a notation yields a natural number, e.g., ω2 yields n2. In other terms, gω2(n)=n2, gα being the slow growing hierarchy. This process of replacement can be made functorial, i.e., apply to morphisms - strictly monotonous functions from m to n; such a functor preserves pull-backs and can be directly extended by means of direct limits: this a dilator. This extension corresponds to the replacement of ω with arbitrary values, e.g., ω+1 or the first non denumerable ordinal Ω, in which case ω2 becomes (ω+1)2 or Ω2. The starting point of the approach was my proof (1975) of the theorem of comparison of hierachies. Let h be your favourite fast growing hierarchy of functions from integers to integers; then h can be expanded into a hierarchy H of functions from denumerable ordinals to themselves. Now, we can relate h (indexed with usual ordinal notations) to H (indexed with the same, in which ω has been replaced with Ω), e.g. hγ vs. HΓ. The two basically agree, i.e., hγ(n)=gHΓ(ω)(n). In particular, the fast growing hierachy up to γ=ε0 is matched by the slow growing one up to the Howard ordinal HΓ(0), where Γ is the first ε number after Ω.