The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme . For example, ACA0 includes the induction axiom . This together with the full comprehension axiom of second-order arithmetic implies the full second-order induction scheme given by the universal closure of for any second-order formula "φ". However ACA0 does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.