Archive for Mathematical Logic 58 (5-6):711-751 (2019)

We introduce and analyze two theories for typed inductive definitions and establish their proof-theoretic ordinal to be the small Veblen ordinal \. We investigate on the one hand the applicative theory \ of functions, inductive definitions, and types. It includes a simple type structure and is a natural generalization of S. Feferman’s system \\). On the other hand, we investigate the arithmetical theory \ of typed inductive definitions, a natural subsystem of \, and carry out a wellordering proof within \ that makes use of fundamental sequences for ordinal notations in an ordinal notation system based on the finitary Veblen functions. The essential properties for describing the ordinal notation system are worked out.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s00153-019-00658-x
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,287
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Proof-Theoretic Investigations on Kruskal's Theorem.Michael Rathjen & Andreas Weiermann - 1993 - Annals of Pure and Applied Logic 60 (1):49-88.
Reflections on Reflections in Explicit Mathematics.Gerhard Jäger & Thomas Strahm - 2005 - Annals of Pure and Applied Logic 136 (1-2):116-133.

View all 9 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A Simplified Functorial Construction of the Veblen Hierarchy.Andreas Weiermann - 1993 - Mathematical Logic Quarterly 39 (1):269-273.
Ordinal Analysis of Non-Monotone-Definable Inductive Definitions.Wolfram Pohlers - 2008 - Annals of Pure and Applied Logic 156 (1):160-169.
Assignment of Ordinals to Patterns of Resemblance.Gunnar Wilken - 2007 - Journal of Symbolic Logic 72 (2):704 - 720.
Ordinal Analysis by Transformations.Henry Towsner - 2009 - Annals of Pure and Applied Logic 157 (2-3):269-280.
Ordinal Diagrams for Π3-Reflection.Toshiyasu Arai - 2000 - Journal of Symbolic Logic 65 (3):1375 - 1394.
Ordinals and Ordinal Functions Representable in the Simply Typed Lambda Calculus.N. Danner - 1999 - Annals of Pure and Applied Logic 97 (1-3):179-201.
Normal Forms for Elementary Patterns.Timothy J. Carlson & Gunnar Wilken - 2012 - Journal of Symbolic Logic 77 (1):174-194.
Σ 1 -Elementarity and Skolem Hull Operators.Gunnar Wilken - 2007 - Annals of Pure and Applied Logic 145 (2):162-175.


Added to PP index

Total views
11 ( #755,588 of 2,325,680 )

Recent downloads (6 months)
1 ( #664,323 of 2,325,680 )

How can I increase my downloads?


My notes