 We have above noted the important fact that in all arithmetical theories \(F\) containing Q, a set is strongly representable in \(F\) if and only if it is recursive, and a set is recursively enumerable if and only if it is weakly representable. Furthermore, one can always take the formula weakly or strongly representing the set to be a RE-formula (i.e., \(\Sigma^{0}_1\)-formula; and, by MRDP Theorem, even an existentially quantified Diophantine equation). It is then natural to require that the set of non-logical axioms of the system at issue is represented by such a formula. If the arithmetized definition of the set of Gödel numbers of axioms reflects how the axioms, if infinite, are inductively defined, the resulting formula will be \(\Sigma^{0}_1\). (For theories which are axiomatizable with finitely many axioms, there is a unique representation of the axioms in the form of a list, and consequently, a unique consistency statement relative to \(\Prov_{FOL}(x)\).) In contrast to determining whether the derivability conditions are satisfied, it is a relatively routine task to determine that a given formula which formalizes the axioms is indeed of the required form (\(\Sigma^{0}_1\)).