A “foundational crisis” occurred already in Greek mathematics, brought about by the Pythagorean discovery of incommensurable quantities. It was Eudoxos who provided new foundations, and since then Greek mathematics has been unshakeable. If one reads modern mathematical textbooks, one is normally told that something very similar occurred in modern mathematics. The calculus invented in the seventeenth century had to go through a crisis caused by the use of divergent series. One is told that by the achievements of the nineteenth century from Cauchy to Cantor this crisis has definitely been overcome. It is well known, but it is nevertheless very often not taken seriously into account, that this is an illusion. The so-called ε-δ-definitions of the limit concepts are an admirable achievement, but they are only one step towards the goal of a final foundation of analysis. The nineteenth century solution of the problem of foundations consists of recognizing, in addition to the concept of natural number as the basis of arithmetic, another basic concept for analysis, namely the concept of set. By the inventors of set theory it was strongly held that these sets are self-evident to our intuition; but very soon the belief in their self-evidence was destroyed by the set-theoretic paradoxes. After that, about 1908, the period of axiomatic set theory began. In analogy to geometry there was put forward an uninterpreted system of axioms, a formal system. This, of course, is quite possible. A formal system contains strings of marks; and a special class of these strings, the class of the so-called “theorems”, is inductively defined.
A Formal System of Axiomatic Set Theory in Coq
