The status of high school geometry

Solution 1:

One can do Euclidean geometry as a completely formal game of symbolic logic. Euclid's axioms are almost sufficient for this, except that they lack formal support for some "obvious" continuity properties such as

Given a circle with center $C$, and a point $A$ such that $|CA|$ is less than the radius of the circle. Then any straight line through $A$ intersects the circle.

David Hilbert, one of the pioneers of the formalist viewpoint, developed an axiomatic system that closes these gaps and allows any Euclidean theorem about a finite number of lines, circles, and points to be proved completely formally. One can work in this system without any reference to arithmetic or set theory, considering Hilbert's geometry axioms as an alternative to, say, ZFC as one's formal basis for one's reasoning.

(Edit: Oops, my history was slightly wrong. Hilbert's axiomatic system was not completely formal. Alfred Tarski later developed a completely formal system; what I say here about Hilbert rightfully ought to read Tarski instead.)

Granted, when one does that one doesn't necessarily think of lines and points as "really existing" in some Platonic sense -- after all, the basic idea of formalism is that no mathematical objects "really exist" and it's all just symbols on the blackboard that we play a parlor game of formal proofs with. But that does not mean that it is necessary, or even desirable, to consider points to be coordinate tuples while playing the game. Indeed, many mathematicians would probably agree that the points and lines of Hilbert's geometric axioms exist "in and of themselves" to at least the same extent that the sets of ZFC (or, for example, the real numbers) exist "in and of themselves".

There are some additional points about this state of things that have the potential to cause confusion, but do not really change the basic facts:

When I speak of Hilbert's axioms as an "alternative" to ZFC, I don't mean that they can be used as a foundation for all of mathematics they way ZFC is -- because they have not been designed to fill that role. I mean merely that they occupy the same ontological position in terms of which concepts one needs to already be familiar with in order to work with them. Perhaps "parallel" might be a better word than "alternative".
The rules of what consists valid formal proofs (in ZFC or geometry) are ultimately defined informally. One may construct a formal model of the rules, but that just punts the informality to the next metalevel, because reasoning about the formal model itself needs some sort of foundation.
When one does formalize the rules of formal proofs, one often does that in a set-theoretic setting. However, this doesn't mean that a different theory such as Hilbert's geometry "depends on" set theory in a fundamental way. Remember that the set theory we use to formalize logic can itself be considered a formal theory, and at some point we have to stop and be satisfied with an informal notion of proof (it cannot be turtles all the way down). And there is no good reason why there has to be a set-theoretic metalayer below the geometry before we reach the inevitable point of no further formalization.
This does not mean that formalizing the rules of formal geometric proof is a pointless exercise. Doing so can tell us things about the axiomatic system that cannot be proved within the formal system itself. In particular, if we formalize the axiomatic system within set theory, we get access to the very strong machinery of model theory to prove facts about the axiomatic system. This is where numbers and coordinates enters the picture, as described in Qiaochu's answer. Using these techniques, one can prove [as a theorem of set theory] that every formal statement about a finite number of lines, points and circles can be either proved or disproved using Hilbert's axioms.
Hilbert's system does not allow one to speak about indeterminate numbers of points in a single statements -- so one cannot prove general theorems about, say, arbitrary polygons. This is by design. The kind of reasoning usually accepted for informal proofs about arbitrary polygons is so varied that formalizing it would probably just end up being a more cumbersome way to do set theory, and there's not much fun in that.

Solution 2:

High school geometry, at its most rigorous, works off of some set of axioms for how points, lines, lengths, etc. should behave. These axioms are modeled by the behavior of points, lines, lengths, etc. in the Euclidean spaces $\mathbb{R}^n$, in the same way that specific groups such as the symmetric groups $S_n$ model the axioms for a group. In other words, the difference between the two points of view is, roughly speaking, the difference between "syntax" and "semantics." Both are parts of ordinary mathematics; neither stands outside of it.

Some things are easier to do syntactically, while others are easier to do semantically. From the perspective of modern mathematics, the major benefit of the semantic perspective on Euclidean geometry is that it allows you to talk about things that go beyond what the traditional axioms are allowed to talk about - things like the Euclidean group and so forth - and is more amenable to interesting and explicit generalizations.

For example, syntactically it's hard to decide whether non-Euclidean geometry makes sense. Semantically, however, it suffices to construct a model of non-Euclidean geometry (e.g. construct hyperbolic space).

Solution 3:

What is taught in high school and elementary school under the label geometry is somewhat of a societal decision. Recently the NCTM (National Council of Teachers of Mathematics) the professional organization for K-12 published a yearbook devoted to geometry which discusses emerging ideas about what is a good choice of content for K-12 geometry. The book is entitled Understanding Geometry for a Changing World (71st yearbook-2009) - Editors Tim Craine and Rheta Rubenstein.

About 20 years ago there was small conference of "research geometers" to discuss ideas for the survey course in geometry for college and how to interface high school and college geometry that COMAP sponsored. The "proceedings" (which I edited) appeared under the title: Geometry's Future (1991). The "book" is out of print but there are copies available in libraries and probably used copies are available. Some of the people whose essays appear are Bill Thurston, Tom Banchoff, Vic Klee, and Marjorie Senechal. There is also this recent item by Carl Lee: www.ms.uky.edu/~lee/nctm2011/nctm2011.pdf

Solution 4:

I encourage you to read this article (link below) by Marvin Jay Greenberg. The two related textbooks are the fourth edition of his Euclidean and Non-Euclidean Geometries and Robin Hartshorne's Geometry: Euclid and Beyond. In short, Hilbert's program was completed by Bachmann and Pejas. One may follow an entirely synthetic approach.

You can download the article itself from MARVIN ... Greenberg won an award for the article, and he is certainly concerned with questions of foundations. In particular, with some care, geometry can be considered entirely without recourse to numbers. Segment arithmetic includes ideas such as line segments being the same length, or one of them longer, but does not require assigning any number to a length. Plus, of course, I am in the article. I helped in writing a little part.

Solution 5:

Thank you everybody for your answers. Here's what I've gathered, feel free to criticize:

For sure, one can do geometry outside of set theory. Hilbert does not presume a background set theory when stating his axioms in his Grundlagen der Geometrie. This said, one can certainly find models of Euclidean geometry within set theory: $\mathbb{R}^2$ and $\mathbb{R}^3$ are the prime examples. Presumably because mathematicians today prefer to work with the full power of set theory, they actually define their Euclidean plane and space as $\mathbb{R}^2$ and $\mathbb{R}^3$. One could say that mathematicians choose to focus on a particular model of geometry, or at most those models that are built inside of set theory. This in fact poses no harm because Euclidean geometry, in Hilbert's form, is categorical: a same statement has the same truth value across all models of Euclidean geometry.

My final point, which is more tenuous and philosophical, concerns the status of the 'intuitive' picture of geometry. I'd like to think we can think of it as yet another model of geometry, one that lives inside the mind, abstracted from the world around us (something similar to what Kant would have to say).

Edit: To define circles, for example, it seems set theoretic language is inevitable. Hilbert says:

I make use particularly of Cantor’s theory of assemblages of points [...] If in our geometry we deﬁne a true circle as the totality of those points which arise by rotating about [a point] $M$ a point diﬀerent from $M$ [...]

So apparently a 'set of points' is also an undefined term in Hilbert's treatment of geometry. I suppose that prior to the scandal that was Russel's paradox, mathematicians did not feel the need to spell out their assumptions about sets explicitly and took them for granted?