 What was still missing was an analysis of the intuitive notion of decidability, needed in the characterization of the notion of an arbitrary formal system. Recall that the set of axioms and the proof relation of a formalized system are required to be decidable. Mathematicians and logicians have implicitly used the intuitive notion of a decision method since antiquity, and as long as one asked for a positive solution, it was sufficient that one presented a concrete method that intuitively striked everyone as a mechanical method. For the general limitative results, such as the general incompleteness theorems, or the undecidability results (see  4.2),  however, a precise mathematical explication of the notion would be needed. Instead of decidable sets or properties, one often considers effective or computable functions or operations, but in fact these are just two sides of the same coin—talk of one can be easily transcribed to talk of another.