 Nor should the precise implications of Gödel’s work be overstated. The order of the quantifiers is important. What Gödel showed is that, for any consistent, recursively axiomatized formal system, F, strong enough for arithmetic, there are truths expressible in purely arithmetical language which are not provable in F. He did not show that there are arithmetical truths which are unprovable in any formal system. Nonetheless, Gödel’s results did hammer some significant nails into the coffin of one version of the deductive ideal of mathematics. There cannot be a single, recursively axiomatizable formal system for all of mathematics which is (a) consistent, (b) purely deductive, and (c) complete. One line of response to this predicament is to explore options for non-deductive methods of justification in mathematics.