A flexible type system for the small Veblen ordinal (Q2312096)

This article provides a proof-theoretic analysis of two impredicative theories of inductive definitions: FIT, a theory of inductively defined functions over an applicative base theory, and TID, a typed subsystem of inductive definitions over arithmetic. Notably, the authors employ so-called `metapredicative' methods only, namely proof-theoretic methods from the realm of predicative proof theory. The two theories FIT and TID are shown to be proof theoretically equivalent and to have proof-theoretic ordinal the small Veblen ordinal, the ordinal \( \vartheta \Omega^\omega\) in the notation of \textit{M. Rathjen} and \textit{A. Weiermann} [Ann. Pure Appl. Logic 60, No. 1, 49--88 (1993; Zbl 0786.03042)]. Lower bounds are proved by presenting well-ordering proofs within the theories for ordinals below \(\vartheta \Omega^\omega\), utilising Schütte's `Klammersymbol' notation system for the small Veblen ordinal. Upper bounds are obtained by embeddings into the second-order system \(\Pi^1_3\text{-RFN}_0 \) of \(\omega\)-model reflection for \(\Pi^1_3\) formulas.