 Another natural and much-studied arithmetical system, which lies between Q and PA in strength, is Primitive Recursive Arithmetic (PRA). It contains not just the above axioms of Q governing successor, addition and multiplication, but also defining axioms for all primitive recursive functions (see the entry on  recursive functions),  and the application of the induction scheme is restricted to quantifier-free formulas (i.e., \(\phi(x)\) is not allowed to contain any (unbounded) quantifiers).