Abstract

An extreme kind of logic skeptic claims that "the present formal systems used for the foundations of mathematics are artificially strong, thereby causing unnecessary headaches such as the Gödel incompleteness phenomena". The skeptic continues by claiming that "logician's systems always contain overly general assertions, and/or assertions about overly general notions, that are not used in any significant way in normal mathematics. For example, induction for all statements, or even all statements of certain restricted forms, is far too general - mathematicians only use induction for natural statements that actually arise. If logicians would tailor their formal systems to conform to the naturalness of normal mathematics, then various logical difficulties would disappear, and the story of the foundations of mathematics would look radically different than it does today. In particular, it should be possible to give a convincing model of actual mathematical practice that can be proved to be free of contradiction using methods that lie within what Hilbert had in mind in connection with his program”. Here we present some specific results in the direction of refuting this point of view, and introduce the Strict Reverse Mathematics (SRM) program.