  Another research direction in proof theory has been to understand how much of impredicative quantification can be explained from principles that are available in intuitionistic mathematics. The strongest such principles are strong forms of inductive definitions. With such principles, one can explain a limited form of an impredicative quantification, called \(\Pi_{1}^1\)-comprehension, where one uses only one level of impredicative quantification over predicates. Interestingly, almost all known uses of impredicative quantifications: Leibniz equality, least upper bound, etc., can be done with \(\Pi_{1}^1\)-comprehension. This reduction of \(\Pi_{1}^1\)-comprehension was first achieved by Takeuti in a quite indirect way, and was later simplified by Buchholz and Schütte using the so-called \(\Omega\)-rule. It can be seen as a constructive explanation of some restricted, but nontrivial, uses of impredicative definitions. 