The Axiomatic View, Formal Proofs, and Mechanizability of Mathematics

Abstract

According to the axiomatic view of mathematics, doing mathematics means primarily proving theorems, that is, producing proofs in a formal system starting from certain axioms. For Hilbert, the main purpose of formalizing mathematics was to provide a secure foundation for mathematics. The axiomatic view was called into question by Gödel’s theorems, which showed that the purpose that Hilbert assigned to the formalization of mathematics could not be achieved. Many supporters of the axiomatic view believe, however, that this should not mean abandoning this view and claim that other results of mathematical logic, such as the Curry-Howard isomorphism, provide sufficient reasons to maintain this view of mathematics. The purpose of this article is to evaluate that claim.