Finitary treatment of operator controlled derivations (Q2743649)

The present paper provides a kind of semantics for the proof-theoretic analysis of impredicative systems, based upon finitary combinatorial techniques. It is part of a research program which started by systematically interpreting Gentzen's finitary reduction steps for first-order arithmetic in terms of \(\omega\)-logic, and it is now applied to the system \textbf{KPi} of admissible set theory with inaccessible universe (for related works, see the papers by the same author reviewed in Zbl 0887.03043 and Zbl 0795.03078).NEWLINENEWLINENEWLINEThe main result is a theorem classifying the bounded multifunctions from the collection HF of hereditary finite sets with values in HF. It is shown that if \(z\) is the set HF, \(\phi\) is a bounded set-theoretic formula and \textbf{KPi} proves \(\forall x \in z \exists y \in z \phi(x,y)\), then there exists a function \(F\) satisfying the following conditions: (i) \(F\) is \(\alpha\)-primitive recursive, for some \(\alpha\) less than the proof-theoretic ordinal \(\psi_\Omega(\epsilon_{I+1})\) of \textbf{KPi} (which is a constructive collapse of the first inaccessible ordinal \(I\)); (ii) \(F\) is a bounding function for \(\phi\), i.e \( \forall n \in \omega \forall x\in L_n \exists y \in L_{F(n)}\phi(x,y) \) is true (in the standard interpretation, \(L_k\) being the constructible hierarchy up to \(k\)). NEWLINENEWLINENEWLINEAfter presenting an infinitary proof system RS\(^\infty\) for ramified set theory, the author introduces the crucial notion of notation system for RS\(^\infty\)-derivations and shows how to build up a family of notation systems (H)\(_\delta\) for RS\(^\infty\)-derivations which are suitably controlled by corresponding ordinal operators H\(_\delta\). In particular, the notation systems are strong enough to represent derivations arising from the embedding of \textbf{KPi} into ramified set theory and from cut-elimination and collapsing procedures. The constructive treatment of ordinals is based on the so-called \(\psi\)-functions and an associated ordinal notation system OT is laid down. In the final step the bounding functions are effectively read off from notations of cut-free derivations of the required \(\Pi^0_2\)-statements. The paper is technically quite complex and yet carefully and neatly written.