  In the current research in the proof theory of second-order  arithmetic, one studies what are known as subsystems of second-order  arithmetic. The strongest results as of today are, in a very brief  outline, the following: let X range over number-theoretic  predicates. A formula such as X(x) states that x  has the property expressed by X. We can now use first- and   second-order logic  to form compound formulas such as  ∀X(Xx ∨ ¬  Xx). The collection of natural numbers for which  such a formula with one universal second-order quantifier holds is  called a  Π11-set  (in this case, the whole of the natural numbers). More generally, a comprehension axiom is of the form  ∃X∀x(Xx  ↔ B(x)). If the formula B has no  second-order quantifiers, the axiom gives what is called arithmetic  comprehension or ACA. If B can have the form  ∀Y∃Z C(x) with no  other second-order quantifiers, the special case of  Π12-comprehension  is obtained. Consistency  proofs for a subsystem of second-order  arithmetic with  Π12-comprehension  have been given by Toshiyasu Arai and Michael Rathjen in the mid-1990s.  (see Rathjen 1995 for these developments).