 As the deducibility of the empty sequent is ruled out if cut elimination holds for GLC (or just the fragment GLC2 corresponding to \(\bZ_2\)), Takeuti’s Fundamental Conjecture entails the consistency of \(\bZ_2\). However note that it does not yield the subformula property as in the first-order case since the minor formula \(F(\{x\mid A(x)\})\) in \((\exists_2\,\rR)\) and \((\forall_2\,\bL)\) may have a much higher (quantifier) complexity than the principal formula \(\exists XF(X)\) and \(\forall XF(X)\), respectively. Indeed, \(\exists XF(X)\) may be a proper subformula of \(A(x)\) which clearly exhibits the impredicative nature of these inferences and shows that they are strikingly different from those in predicative analysis where a proper subformula property obtains.