Induktive Definitionen und Dilatoren. (Inductive definitions and dilators) (Q1101106)

The paper contains a new and comparatively simple proof of the following theorem by Girard: ``If \(\Sigma \vDash_ I\phi\) (and \(\Sigma\) is recursive) then there exists a (recursive) dilator D such that \(\Sigma \vDash_ I \phi^{\alpha,D(\alpha)}\), for all \(\alpha\in On.''\) [\textit{J.-Y. Girard}, Logic, methodology and philosophy of science. VI, Proc. 6th Int. Congr., Hannover 1979, Stud. Logic Found. Math. 104, 89-107 (1982; Zbl 0496.03038)]. Here \(\Sigma\) is an axiom system in some countable first order language L, and \(\phi\) is a formula which besides the symbols of L may also contain constants \(P_{{\mathfrak A}}\) for inductively defined sets of individuals. The meaning of \(\Sigma \vDash_ I \phi\) is that \(\phi\) holds in every \(L_{ID}\)-structure (with \(L_{ID}:=L\cup \{P_{{\mathfrak A}},...\})\) which is a model of \(\Sigma\) and associates with each \(P_{{\mathfrak A}}\) its standard interpretation. \(\phi^{\alpha,\beta}\) designates the formula obtained from \(\phi\) by replacing each negative (positive) occurrence of \(P_{{\mathfrak A}}\) by \(P_{{\mathfrak A}}^{<\alpha}\) \((P_{{\mathfrak A}}^{<\beta}\) resp.). The constants \(P_{{\mathfrak A}}^{<\alpha}\) are interpreted in the natural way, i.e. by the \(\alpha\)-th stage of the inductive defnition \(P_{{\mathfrak A}}\). Girard's theorem has some significant recursion theoretic corollaries, for example: ``If F is a function \(uniformly\)- \(\Sigma\) \({}_ 1\) over all admissible sets then F is E-recursive. If G: On\(\to On\) is \(uniformly\)-\(\Sigma\) \({}_ 1\) over all admissible sets then G is (\(\infty,0)\)-recursive.'' [\textit{J. Van de Wiele}, Logic colloquium '81, Proc. Herbrand Symp. Marseille 1981, Stud. Logic Found. Math. 107, 325-332 (1982; Zbl 0499.03035)]. Therefore it seems desirable to have an easy and direct proof of this theorem as provided by the present paper. The essential point here is the very direct definition of the dilator D. By generalizing the method of \textit{K. Schütte} for proving the completeness of first order predicate logic [Proof theory (1977; Zbl 0367.02012)], for each \(L_{ID}\)-formula \(\phi\) an (infinitary) formula tree \(T_{\phi}\) is constructed in such a way that \(T_{\phi}\) is wellfounded if and only if \(\Sigma \vDash_ I \phi\) holds. In that case \(T_{\phi}\) can be considered as an (essentially) cutfree derivation of \(\phi\) from \(\Sigma\) within a certain infinitary system of ``inductive logic'' (which in fact is a modification of a system due to Girard). Moreover, \(T_{\phi}\) turns out to be a [0,\(\Omega\) [-homogeneous tree in the sense of \textit{H. R. Jervell}, Logic colloquium '81, Proc. Herbrand Symp. Marseille 1981, Stud. Logic Found. Math. 107, 147-158 (1982; Zbl 0503.03027)], and one easily shows that, for all \(\alpha\in On\), \(\Sigma \vDash_{ID} \phi^{\alpha,\alpha '}\) holds, where \(\alpha\) ' denotes the Brouwer-Kleene length of \(T_{\phi}[\alpha]\). This yields the above theorem, since every wellfounded [0,\(\Omega\) [-homogeneous tree T induces canonically a dilator D with D(\(\alpha)\) \(= Brouwer\)-Kleene length of T[\(\alpha\) ].