Transfinite type theory and provability of second order formulas (Q1238797)

Given a non-empty set \(D\), we can define \(\mathfrak D(\alpha)\) for each ordinal \(\alpha\), in the following manner: 1.\ \(\mathfrak D(0) =D.\;2.\;\mathfrak D(\alpha+ 1)=P^*(\mathfrak D(\alpha)).\;3.\;\mathfrak D (\alpha)= P^*({\underset{\beta<\alpha}\bigcup}\mathfrak D (\beta))\) , where \(\alpha\) is a limit ordinal. (\(P^*(M)\) denotes the set of all predicates over \(M\).) For each \(\alpha\), we can consider the logic which treats, as objects, not only elements of \(D\) but also elements of \(\mathfrak D(0),\mathfrak D(1),\dots,\mathfrak D(\alpha)\). The author gives a formal system \(\mathfrak H(\alpha)\) which is a formalization of the logic. The main theorem is, roughly speaking, as follows: Let \(\mathfrak P(\alpha)\) denote the set of provable second order formulas in \(\mathfrak H(\alpha)\). If \(\alpha<\omega^\omega\), then \(\mathfrak P(\alpha)\subsetneqq\mathfrak P(\alpha+1)\) .