 This drawback, among other things (see Feferman 1997), led Solomon Feferman in the late 1950s to look for an alternative line of attack to the second theorem (see Feferman 1960). Feferman approaches the issue in two steps: First, he isolates the formulas \(\Prov_{FOL}(x)\) which arithmetize some standard notion of derivability in first-order logic in order to allow us to fix one chosen formula for provability in logic. How the set of non-logical axioms of the system at issue are presented is left open at this stage. Secondly, Feferman looks for a suitable constraint for presenting the axioms. Among the formulas of the language of arithmetic, he isolates what he calls PR- and RE-formulas; the former correspond to the canonical primitive recursive (PR) definitions in arithmetic, and the latter to existential generalizations of the former. Every recursively enumerable (RE) set can be defined by a formula of the latter sort; these are just the \(\Sigma^{0}_1\)-formulas. These two classes are easy to discriminate purely by their syntactical form. (In fact, by the MRDP Theorem (see below), one could—instead of RE-formulas—focus on even simpler class of existentially quantified Diophantine equations.)