 However, essentially the same system is obtained if one takes just the axioms of Q and the induction scheme restricted to, roughly, purely existential formulas (in technical terms,  \(\Sigma^{0}_1\)-formulas; see below) (this was first showed by Parsons 1970). Moreover, \(\Sigma^{0}_1\)-induction can be shown (Paris and Kirby 1978) to be equivalent to the induction scheme restricted to (roughly) purely universal formulas \((\Pi^{0}_1\)-formulas). PRA can also be formulated as a “logic-free” equational calculus. PRA, or something equivalent to it, is sufficient for developing the theory of syntax for formalized theories. It is often taken as the unproblematic background theory in which various other systems, whose legitimacy may be more controversial, are studied.