I am reading about the 1900s revolution of math pioneered by figures such as Hilbert. I have seen many articles speak very fondly of these figures due to the fact they tried to study Mathematics through the perspective of Logic.
I do agree that it was great... but wasn't this perspective already put forward by Euclid when he tried to do axiomatic Geometry? What did the 1900s proof theory achieve that Euclid couldn't?
For example, the very first proposition: Construct an equilateral triangle $ABC$, where one side $AB$ is given.
Euclid says
Draw a circle with center $A$ and radius $AB$. [By Postulate 1]
Draw the circle with center $B$ and radius $BA$. [By Postulate 1]
Let $C$ be a point where the two circles intersect.
But there is nothing in Euclid that proves the two circles intersect at all.
"Look at the picture, it's obvious" is not considered rigorous.
"A is inside the circle $BCD$, and $E$ is outside the circle $BCD$, so there must be a point of circle $ACE$ exactly on the circle $BCD$." There is no basis in Euclid to make that assertion.
The main difference is that Mathematical logic and set theory did not exist at the time of Euclid. (The Logic of Aristoteles is still very far from mathematical logic created in 19th century). As a result, Euclid's Elements are not completely rigorous from the modern (and early 20th century) point of view: for example, Euclid did not state all axioms which he really used (the first complete from the modern view set of axioms for Euclid was formulated by Hilbert). There are actual gaps in Euclid's reasoning which in principle could be detected during the 24 centuries since Euclid but were not detected. For example, Cauchy's theorem on convex polytopes. It is a deep theorem which fills one of these gaps, but the gap was not even recognized before Cauchy.
The reason of this was that without rigorous mathematical logic, complete analysis of Euclid's axiomatic system was not possible. Understanding of relation between geometry and numbers at the time of Euclid was also very incomplete.
The hope of Hilbert was that once correctly formalized, it would be possible to show that mathematics was sound and that any statement has a proof. Godel's incompleteness results put an end to that hope, at least for recursively enumerable theories strong enough to recover arithmetic.
A large part of Euclid's Elements, namely the geometric part, does not assume arithmetic but can actually be built on first order logic. Several axiomatics were devised circa 1900 to dispel a few gaps in the treatise of Euclid, mostly due to a lack of treatment of order on lines, corresponding to a point being between two other points. Amongst the many axiomatics developped at that time, the one introduced in the "Grundlagen der geometrie" by Hilbert is the most famous. The big result was yet to come.
Alfred Tarski gave a slightly different axiomatic for elementary geometry, of a more logical nature, and relying only on first order logic. He was then able to show that his theory of elementary geometry is
-- consistent: a well formed statement is either true or false, and cannot be both.
-- complete: a proposition (or its negation) stated in the language of first order logic always has a proof.
-- algorithmically decidable: there is an explicit algorithm that decides if a statement is true or false.
So, Alfred Tarski realized Hilbert's program in the context of elementary geometry and showed what mathematicians have anticipated for more than two millenia: the logical perfection of Euclid's geometry.
