  In 2010, Vladimir Voevodsky gave a lecture on "What If Current Foundations of
Mathematics Are Inconsistent?" Among other things he said that he was seriously
suspicious that an inconsistency in PA (first-order Peano arithmetic) might
someday be found. About a year later, Edward Nelson announced that he had
discovered an inconsistency not just in PA, but in a small fragment of
primitive recursive arithmetic. Soon, Daniel Tausk and Terence Tao
independently found a fatal error, and Nelson withdrew his claim, stating that
consistency of PA was an "open problem." Many mathematicians may find such
claims bewildering. Is the consistency of PA really an open problem? If so,
would the discovery of an inconsistency in PA cause all of mathematics to come
crashing down like a house of cards? This expository article attempts to
address these questions, by sketching and discussing existing proofs of the
consistency of PA (including Gentzen's proof and Friedman's relative
consistency proof that appeals to the Bolzano-Weierstrass theorem). Since
Nelson was a self-avowed formalist, the article also examines the implications
of formalism.
