The Empirical Metamathematics of Euclid and Beyond
Euclid’s Elements is an impressive achievement. Written in Greek around 300 BC (though presumably including many earlier results), the Elements in effect defined the way formal mathematics is done for more than two thousand years. The basic idea is to start from certain axioms that are assumed to be true, then—without any further “input from outside”—use purely deductive methods to establish a collection of theorems.
Euclid effectively had 10 axioms (5 “postulates” and 5 “common notions”), like “one can draw a straight line from any point to any other point”, or “things which equal the same thing are also equal to one another”. (One of his axioms was his fifth postulate—that parallel lines never meet—which might seem obvious, but which actually turns out not to be true for physical curved space in our universe.)
On the basis of his axioms, Euclid then gave 465 theorems.
Now I wish I could read greek…