14
$\begingroup$

In David Hilbert's 1899 Grundlagen der Geometrie, Hilbert gives a rigorous axiomatization of Euclidean geometry. As I understand it, some of Hilbert's axioms must be expressed in second order logic (for example his "Euclid's axiom") and as his system contains some notion of arithmetic (this is perhaps not correct?), by Gödel's first incompleteness theorem this means that Hilbert's axiomatic system is incomplete (meaning that there exist statements expressed by the vocabulary of the system that cannot be proven to be true) and by Gödel's second incompleteness theorem, his system cannot demonstrate its own consistency.

Later, Tarski gave his own axiomatization of Euclidean geometry that is entirely in first order logic so by Gödel's completeness theorem, it can demonstrate its consistency, it is decidable and complete.

Is the above accurate and if so, is Tarski's axiomatic system still inferior in some ways to Hilbert's (with a lack of expressive power or doesn't cover the entire Euclidean geometry as we understand it)?

$\endgroup$
10
  • 1
    $\begingroup$ Wait, are the incompleteness theorems not delicious pickled gherkins? I really need to re-read my logic books.... $\endgroup$ Feb 23, 2014 at 18:51
  • 2
    $\begingroup$ The completeness (and decidability) of Tarski geometry is by no means a consequence of the Godel Completeness Theorem. In fact "completeness" has two entirely different meanings in the two results. The completeness of Tarski geometry is usually done by a quantifier elimination argument. $\endgroup$ Feb 23, 2014 at 18:57
  • 1
    $\begingroup$ Roughly Godel Completeness says that the usual logical axioms are enough to prove all the sentences that are true in every model of a theory $T$. The theory itself could be very incomplete, like Group Theory. Completeness of Tarski geometry says that for any sentence $\phi$ of the theory, either $\phi$ is a theorem or $\lnot\phi$is a theorem. $\endgroup$ Feb 23, 2014 at 19:04
  • 2
    $\begingroup$ @AsafKaragila "I have no idea why you would believe anything like that."In that case I'm happy to explain why: I am a third year uni student and my knowledge of mathematics is limited, sometimes I believe things which are inaccurate or simply wrong, like here. I hope it will improve after using SE more to learn math. "Or maybe, just maybe, it has a lot to do with the logic that you are working in? I don't know. You tell me." I can't tell you because I don't know. I asked this question is to learn more about this GIT and axiomatizations of Euclidean geometry, not to inform others. (continued) $\endgroup$
    – Sid
    Feb 23, 2014 at 21:12
  • 7
    $\begingroup$ @AsafKaragila So I really appreciate your answers to my questions, but I think that your tone is maybe a little unnecessarily unfriendly! But if you want to continue explaining things to me, could you please tell me (if you know) if GIT has anything at all to do with Hilbert's axiomatization of Euclidean geometry? Also (just wondering), why do mathematicians not work in second-order logic if they can avoid GID that way? If you think this is too unrelated to my question, I'd be happy to discuss it in a chatroom. $\endgroup$
    – Sid
    Feb 23, 2014 at 21:17

1 Answer 1

21
$\begingroup$

Hilbert's axioms predate the development (or at least the wide adoption) of fully symbolic logic, so they are expressed in partially informal language -- though Hilbert strove to make them as precise as he could.

They include the Axiom of Archimedes, formulated in language that presupposes that the natural numbers are already known. As such, if we want to formalize the system in a modern sense, we'd need to add in some machinery for talking about integers, and it would be somewhat hard to avoid making that machinery powerful enough that Gödel's theorem would apply to it.

Furthermore, there's also an Axiom of Completeness which attempts to claim directly that the structure we're speaking about is maximal in a certain technical sense. In the modern view of formal theories, this hardly qualifies as an "axiom" at all, because it doesn't assert the truth of any formula interpreted inside the language of the theory itself. In modern terms, it appears to try to say that every existential formula of a certain shape that is true in some model of the other axioms must itself be elevated to axiomatic status.

However, it is not clear that "formulas that are true in some model of the other axioms" are even recursively enumerable -- which means that Hilbert's axioms, interpreted in this way, are not effective. In other words there's no systematic way to check whether a purported proof is valid or not. Therefore Gödel's incompleteness theorem does not apply to Hilbert's axioms. It seems at least plausible that if we interpret them inside set theory in the above sense, they do have $\mathbb R^3$ as their only model up to isomorphism. (That is, whatever the set theory in question considers $\mathbb R^3$ to be).

Tarski's axioms for geometry were created after formal logic was better developed. They form a genuine, effectively axiomatized, first-order theory, with no ad-hoc appeals to integers, sets, or model theory. They manage to be a complete theory because they are not strong enough to express or simulate arithmetic.

The price paid for the completeness in Tarski's case is that the language the axioms are formulated in is not expressive enough to speak of even finite sets of points, or for example general polygons. Every theorem has to be proved separately for triangles, quadrilaterals, pentagons, and so forth.

This restriction is unavoidable for a complete theory, because as soon as we extend the language with a way to speak of finite sets of points and lines in a reasonable way, we can use those sets as proxies for natural numbers (each set representing the number of points in it) and begin to speak about enough arithmetic that Gödel's incompleteness theorem will apply to it.

Later, Tarski gave his own axiomatization of Euclidean geometry that is entirely in first order logic so by Gödel's completeness theorem, it can demonstrate its consistency, it is decidable and complete.

As mentioned in the comments, this is a complete misunderstanding of what the completeness theorem says. Tarski's geometry cannot even speak about its own consistency, much less prove it.

$\endgroup$
5
  • $\begingroup$ Thanks a lot for your answer, I wish everyone could be this helpful. I am writing a term paper and would like to discuss this, do you have a reference where I can read about this in more detail? In particular, I would like to write that Tarski's axioms were created after formal logic was better developed (like you said) and be able to cite a good source. $\endgroup$
    – Sid
    Feb 23, 2014 at 22:43
  • 1
    $\begingroup$ @Sid: I don't have a good reference (I'm just reading the Wikipedia articles as I go along), but the timeframe issue is fairly easily settled. Tarski's axioms were first published in 1958-59, long after first-order logic was well-defined enough for Gödel to prove his completeness theorem in 1930. By 1958, what a first-order theory is was textbook material (the first edition of Church's Introduction to Mathematical Logic was in 1944). On the other hand, Hilbert's axioms are from 1899, before even Principia Mathematica. $\endgroup$ Feb 23, 2014 at 22:58
  • $\begingroup$ The Tarski result on the completeness/decidability is pre-war (WWII). $\endgroup$ Feb 24, 2014 at 7:49
  • $\begingroup$ @André: I see now that the history is deeper than it looked to me at first glance. The sources do seem to say that he kept tinkering with the system until the late 1950s. $\endgroup$ Feb 24, 2014 at 10:56
  • $\begingroup$ @Henning: Would you say that Hilbert’s axiomatization of Euclidean geometry is an instance of soft axiomatization? For example, in soft axiomatization, a group is described as a triple $ (G,\cdot,e) $, where $ G $ is a set, $ \cdot: G \times G \to G $ and $ e \in G $, with $ \cdot $ and $ e $ satisfying the group properties. In hard axiomatization, one defines the first-order language of group theory, which consists of a binary function symbol $ \cdot $ and a constant symbol $ e $ that represent group multiplication and the identity element respectively, and then states the group axioms. $\endgroup$ Aug 28, 2016 at 23:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .