 Our Comprehension Axiom Schema is impredicative in the sense that the bound n-ary relation variables which may potentially occur in the formula \(\phi(a_1,\ldots, a_n)\) have R in their range. In this sense second-order logic is utterly impredicative. The Comprehension Axiom Schema has weaker forms that are less impredicative. In the Arithmetic Comprehension Schema we assume \(\phi(a_1,\ldots, a_n)\) is first order. In the \(\Pi^1_1\)-Comprehension Schema we assume \(\phi(a_1,\ldots, a_n)\) is \(\Pi^1_1\). In mathematical practice these two weaker principles usually suffice, see Simpson (1999 [2009]) and  §14.