Universes over Frege structures (Q1861539)

The author determines the proof-theoretic strengths of FSU (the theory of Frege structures with universes) with three forms of (mathematical) induction. FSU itself is built on an applicative theory with the truth predicate \(T(\cdot)\), and inductions are labelled C-In (class induction), T-In (truth), and F-In (formula). The last, F-In, begins with \(\varphi(0) \wedge \dots\) for any formula \(\varphi\), T-In with \(T(f0)\wedge\dots\) where \(f\) is a variable, and C-In has an additional formula `if \(f\) is a class' before \(T(f0) \wedge\dots\). The strengths of FSU+C-In, of FSU+T-In and of FSU+F-In are shown to be the same as those of the theories of inductive definitions \(\widehat {\text{ID}}_{<\omega}\), \(\widehat{\text{ID}}_{<\omega^\omega}\), and \(\widehat {\text{ID}}_{<\varepsilon_0}\), respectively. The proof goes in two ways, of course. The author gives a translation of the ID-language into the FSU-language. In the other direction, the FSU systems are put into an infinitary system, and term models are handled in relevant ID theories. The author gives not just technical accounts, but writes in a wider context, beginning with Frege structures, and including recent activities at Bern, and other results.