 After Gentzen, it was Gaisi Takeuti who worked on a consistency proof for \(\bZ_2\) in the late 1940s. He conjectured that Gentzen’s Hauptsatz not only holds for first order logic but also for higher order logic, also known as simple type theory, STT. This came to be known as Takeuti’s fundamental  conjecture.[18]  The particular sequent calculus he introduced was called a generalized logic calculus, GLC (Takeuti 1953). \(\bZ_2\) can be viewed as a subtheory of GLC. In the setting of GLC the comprehension principle CA is encapsulated in the right introduction rule for the existential second-order quantifier and the left introduction rule for the universal second-order quantifier. In order to display these rules the following notation is convenient. If \(F(U)\) and \(A(a)\) are formulae then \(F(\{v\mid A(v)\})\) arises from \(F(U)\) by replacing all subformulae \(t\in U\) of \(F(U)\) (with U indicated) by \(A(t)\). The rules for second order quantifiers can then be stated as  follows:[19]