Not every consistent body of propositions can be captured by a describable collection of axioms. In recursion theory, a collection of axioms is called recursive if a computer program can recognize whether a given proposition in the language is a theorem. Gödel's first incompleteness theorem then tells us that there are certain consistent bodies of propositions with no recursive axiomatization. Typically, the computer can recognize the axioms and logical rules for deriving theorems, and the computer can recognize whether a proof is valid, but to determine whether a proof exists for a statement is only soluble by "waiting" for the proof or disproof to be generated. The result is that one will not know which propositions are theorems and the axiomatic method breaks down. An example of such a body of propositions is the theory of the natural numbers, which is only partially axiomatized by the Peano axioms (described below).