Constructibility of the 17-gon

A few days ago I stumbled on the GeoCoq Project, which is a project on the formalization of geometry in the proof-assistant Coq. I contacted one of the people involved (Julien Narboux) in the hopes he could finally provide an answer to this question. He kindly replied to me and sure enough, I think the quesion is at last settled for me.

For some context I will first give the essential content of my mail and then his answer.

---

Me: This question came to my mind when I was taking a lecture on algebra, in which we showed the standart result by Gauss, which states the constructibility of the 17-gon. My still prevailing gut feeling is that, since this was done using complex numbers, it only establishes that the statment holds in one model of euclidean geometry, which shows its satisfiability but says nothing more concerning the provability.

---

Julian: You are right, when doing a proof using algebraic means per se, you only prove that the statement is true in the Cartesian plane over some field, you show that the statements holds in one model of the axioms.

To transfer the result to any model, you need a meta-theoretical result about the models of your axiom system. This is the main result of both Tarski and Hilbert’s books (Foundations of Geometry, and Metamatematische Methoden in der Geometrie).

Starting from Hilbert axioms, Hilbert’s defines (following Descartes; addition and multiplication by geometric means, and then shows he has a field). As soon as you have a field, you can define coordinates (by projecting on two perpendicular lines). Then one can prove by geometric means that the characterization of geometric predicates by algebraic equations is correct. This is the definition of the Cartesian plane over a field.

Then depending on the axiom of continuity one assumes you get a different field: with Tarski’s and Hilbert’s axiom (without Group V of Hilbert), the field is always Pythagorean. If you add the continuity axiom (Group V) the field has to be isomorphic to the reals. For Tarski’s axioms, the axiom of continuity is weaker and you get an algebraic closed field.

So in principle yes, an algebraic proof of the constructibility of some statement can be transferred into a purely synthetic proof using Hilbert axioms. But if you "unfold" the geometric definitions of the operators in the algebraic proof then you would obtain an enormous construction. For the 17-gon, I guess it would be possible to prove that the construction you cite is ok by algebraic means, and checking this proof in Coq would give you an actual proof from the Hilbert and Tarski’s axioms.

We have done this for the 9 points theorem (line 1531 of following Code). We prove it automatically using groaner basis, but we use our proof that we can define algebra inside geometry, to obtain a proof which is valid from Tarski’s axioms (we have shown that Tarski’s and Hilbert’s axioms, excluding continuity, are equivalent).

All of this is explained in the following papers:

• About the link between algebraic and geometric proof, there is this paper by Michael Beeson.

• We have done what Michael was proposing in 2012, and have formalized the algebraization or arithemtization of geometry.

---

TL;DR Some meta-theorems about the proof systems indeed guarantee us the provability when we can provide algebraic constructions.

Disclaimers (6 November 2020): I deleted this post a few years ago but it was recently undeleted by three other users. It has been pointed out to me that authors don't "own" their material after it is posted here, and so I will bow to the will of the community and leave the post undeleted, but I would like to add a few remarks.

1. Since this post was undeleted it has attracted some downvotes. To future downvoters: I am very interested in receiving critiques of the arguments I make in this answer. If there is some flaw, I would, of course, like to know what it is.

2. As I thought more about the issues over time, I kept adding to this answer. The additions appear in reverse chronological order because I wanted my most up-to-date thoughts to appear on top. If you want to read the text in the sequence it was written, start with the bottom-most boldface heading and work up.

3. The original version of this question had the title "Would Euclid be satisfied by the construction of the $17$-gon given by Gauss?" and contained the query "Does the algebraic proof that an $n$-gon can be constructed, also show that there is a proof, of the constructibility, which only uses the Axioms of Euclidean geometry? (or Hilbert's Axioms)". It was in this spirit that I drafted my answer, attempting to roughly sketch a mechanical procedure for turning Gauss's argument into a geometric proof using ingredients based on Euclid's Elements. My answer isn't so suitable for the current version of the question, which is narrower, focusing on Hilbert's axioms.

4. Any answer to the current version of the question should address how Hilbert's axioms connect with the classical construction tools (compass and straightedge). Hilbert's axioms say nothing about circles or compasses. I believe the Poncelet–Steiner theorem may be relevant here, but I am not expert enough to address that at present, unfortunately.

5. The proof sketched here has a structure that some may find worrisome, although I believe it to be okay: it assumes the existence of the regular $n$-gon even though this might not be constructible. This existence assumption can, I believe, be avoided, but it is useful if one is seeking a direct translation of Gauss's algebra into geometry. In coordinate geometry, with the usual ways of computing distances and angles (which are consistent with either Euclid's or Hilbert's axioms), the existence of the regular $n$-gon is straightforward to establish. Hilbert's axiom of line completeness would then seem to allow this result to be imported directly into his system. (Again, I am not and expert in this, so please let me know if I am mistaken.) In Euclid's system, the explicitly stated axioms do not seem to address such existence questions, but it is now understood that Euclid used a number of unstated axioms. Proclus, who wrote more than 700 years after Euclid, seems to have thought that Euclid used construction to establish existence, and some more modern scholars have argued similarly, but experts I have great respect for, such as Wilbur Knorr, have concluded that this is not the case. Euclid's construction of the regular pentagon is a case in point: it very much follows the analysis-synthesis schema common in Greek mathematics, in which first a figure (whose existence is never questioned) is analyzed to determine a set of properties its components must satisfy, and second, in the synthesis stage, objects satisfying those properties are constructed leading to the construction of the original figure. What Gauss does is analogous, focusing entirely on the analysis stage; the synthesis stage is obvious from the work of Descartes (and really, from the work of the Greeks themselves).

Further addition (21-24 January 2018): This may be well-known to you, but in case not, here's a geometric construction, with proof, of the roots of a certain type of "quadratic equation". (Gauss's method involves repeated solution of this type of quadratic equation.) I've added below some diagrams showing some of the Gaussian periods, in the hope that this will make clear that they can be defined and their properties proved by geometric methods. There are still many details that would need to be filled in, however.

Consider the figure below consisting of two perpendicular lines meeting at $O$, with given line segments $OD$, $OP$, and $OC$. (The line segment $OP$ will play the role of unit length.) The goal is to construct a point $A$ on line $DC$, on the same side of $O$ as $D$, and a point $B$ on line $OP$, on the same side of $O$ as $P$, such that $OAD$ is similar to $OPB$, or, in other words, so that $OA$ is in the same ratio to $OD$ as $OP$ is to $OB$, with the further condition that $OB$ exceeds $OA$ by a length equal to $OC$. Note that if $OD$ has length $d$, $OP$ has length $1$, $OC$ has length $c$, $OA$ has length $x$, and $OB$ has length $y$, then this amounts to solving the system $xy=d$, $y=x+c$, or $x(x+c)=d$. Note also that the similarity condition is equivalent to equality of the areas of the rectangle with sides $OA$, $OB$ and the rectangle with sides $OD$, $OP$.

The method is as follows: construct $P'$ on line $DC$ on the same side of $O$ as $C$ the same distance from $O$ as $P$. Construct the semicircle $DRP'$. Note that the area of the square on $OR$ is equal to that of the rectangle with sides $OD$, $OP$. Construct $HR$, where $H$ bisects $OC$. Let the arc with center $H$ and radius $HR$ intersect line $DC$ at $A$ (on the same side of $O$ as $D$). Construct $A'$ on line $OP$ (on the same side of $O$ as $P$) so that $OA$ and $OA'$ have equal length. Finally construct $B$ on line $OP$ so that $OB$ exceeds $OA'$ by a length equal to that of $OC$.

To prove that this works, observe that the square on $AH$ equals the square on $HR$, which, by the Pythagorean Theorem, equals the sum of the squares on $OR$ and on $OH$. The square on $OR$ therefore equals the gnomon $OJK$, which in turn equals rectangle $AB$. Since the square on $OR$ equals rectangle $DP$, rectangle $DP$ equals rectangle $AB$, as was to be shown.

Given a regular $17$-gon, we can define the Gaussian periods geometrically, and prove the needed properties. Shown below are $eta^{(2,17)}_0$ and $eta^{(2,17)}_1$, using $r=3$ as primitive root.

The line segment $OA$ corresponds to $eta^{(2,17)}_0$ and the line segment $OB$ to $eta^{(2,17)}_1$. The polygons on these line segments are built from line segments congruent and parallel to the radial lines emanating from $O$. The polygon on $OD$ is similar to the polygon on $OB$. What is needed is to show that the length of $OB$ exceeds that of $OA$ by an amount equal to the length of $OP$ and that $OD$ is four times the length of $OP$. The figure below might suggest a geometric proof of the latter statement.

As I said, I am happy to elaborate further if needed. I am beginning to suspect, however, that I do not grasp what the sticking point really is. To try to understand, I went back and read the early versions of the original post. It seems that there is some objection to proofs that construct the regular $n$-gon by constructing the length $cos(2pi/n)$. I do not understand what the objection is, as long as this length is defined in purely geometric terms.

In Version 1 of the original post, I also find the following, somewhat mysterious statement

A week later, someone in the class did find a solution by geometric reasoning, which used the fact that the exercice is implicitly saying that the regular 5-gon is constructable.

It's probably a failure of imagination on my part, but I find it hard to see how the assumption of constructibility of the regular $5$-gon could help in its construction. On the other hand, the kind of proof I have in mind works most simply if one assumes existence of the regular $5$-gon. Is it possible that you meant to say that existence was assumed, and not constructibility? Here's a possible logical structure for a proof: given a regular $n$-gon, identify a line segment from which the $n$-gon can be constructed and prove some properties of that line segment. Then provide a construction of a line segment satisfying those properties, and prove that the line segment constructed is the unique solution to the problem. Is there some objection to this kind of proof? (Not to imply that I think the proof has to follow this structure, but it makes things a lot simpler.)

Added (2 October 2016): Perhaps my original answer was too non-specific to be useful. I think the question comes down to that of whether there is some difference between the $5$-gon and $17$-gon such that the $5$-gon can be constructed with geometry alone, but the $17$-gon needs algebra.

Terms such as $cosfrac{2pi}{n}$, $cosfrac{4pi}{n}$, and so on would not have been in Euclid's vocabulary. Nor would the concepts of negative or complex numbers. In fact, Euclid would not have accepted the idea of associating numbers with lengths, areas, or angles. Numbers for Euclid were $2$, $3$, $4$, ... Euclid did, however, make use of Eudoxus's sophisticated theory of proportion, which, when applied to magnitudes, including lengths, would have allowed him to perform manipulations equivalent in many ways to our own.

So Euclid could have understood $cosfrac{2pi}{n}$, $cosfrac{4pi}{n}$, and the like as line segments obtained by orthogonal projection of different radii of the regular $n$-gon (of radius $1$) onto an axis through one of its vertices. Since the Greeks didn't recognize negative magnitudes, that some of these cosines are negative would have to have been handled by a, perhaps cumbersome, case analysis.

Gauss's method, applied to the constructibility of the pentagon, seems to hinge on two facts:

1. that both the sum and the product of the unknown magnitudes $cosfrac{2pi}{5}$ and $cosfrac{4pi}{5}$ are known magnitudes;
2. that if the sum and product of two unknown magnitudes are known, both unknown magnitudes can be constructed.

The computation of Fact 2 can be carried out geometrically using standard quadrature methods of Greek geometry. I don't know of any evidence that Greeks of Euclid's era solved this problem in generality, or even thought about it, but it is clear that the tools were present, and that one could provide a construction and a demonstration that would satisfy them, if required.

This leaves Fact 1. That the sum of $cosfrac{2pi}{5}$ and $cosfrac{4pi}{5}$ is $-frac{1}{2}$ has a straightforward geometric proof (with $cosfrac{2pi}{5}$ and $cosfrac{4pi}{5}$ interpreted as particular line segments, as suggested above).

Proving that their product is $-frac{1}{4}$ is easy algebraically: express both cosines in terms of fifth roots of unity and fully expand the product. This calculation makes use of three ingredients, (1) complex multiplication, (2) complex addition, and (3) the distributive law. One could define complex multiplication geometrically in terms of angle addition and rescaling of line segments, both of which can be carried out geometrically. (That the rescaling can be carried out using compass and straightedge was emphasized by Descartes in his development of analytic geometry, but I don't think would have been a surprise to the Greeks at all.) Complex addition can clearly be defined geometrically as well. Proving the distributive law shouldn't present any conceptual difficulties: it will make use of properties of similar triangles.

If one accepts all of the foregoing, the question becomes whether there is anything different in principle about the $17$-gon. The main difference that I see is that it is no longer the sum and product of two cosines that are known magnitudes, but rather the sum and product of magnitudes equal to sums of four cosines. But these sums of four cosines can be understood geometrically as particular line segments related to the $17$-gon. Sums and products of these can be understood geometrically, exactly as for the $5$-gon. One then has to repeat the process two more times, first on magnitudes equal to sums of two cosines, and finally on single cosines.

Once it has been established that the sum and product of certain unknown magnitudes equal certain known magnitudes, one may then proceed to construct the unknown magnitudes. This ultimately produces all of the cosines for the $17$-gon, again understood as particular line segments.

Original answer (11 August 2016): Given a unit of length and segments of various lengths, one can, using compass and straightedge, construct sums, differences, products, quotients, and square roots of lengths. This was emphasized by Descartes, but all the techniques involved were known to and used by the ancient Greeks.

Given the unit circle in the complex plane, the regular $n$-gon inscribed in the circle can be constructed if we can construct the length $cos(2pi/n)$. (Complex numbers, which were unknown to the ancient Greeks, are introduced only for convenience and are not essential.) For we can then construct the point in the complex plane corresponding to the number $cos(2pi/n)$, and, by constructing a perpendicular to the real axis at this point, the point $omega=e^{2pi/n}$. The complex numbers $1$, $omega$, ... $omega^{n-1}$ can then be constructed by repeating the procedure, and form a regular $n$-gon.

That $omega$, $omega^2$, ..., $omega^{n-1}$ satisfy the algebraic equation $x^{n-1}+x^{n-2}+ldots+x+1=0$ can be translated into geometrically provable statements about the vertices of the regular $n$-gon. Specializing to the case where $n$ is a prime of the form $2^k+1$, we define the quantities $$ eta^{(2^ell,n)}_i=sum_{j=0}^{2^{k-ell}-1}omega^{r^{(2^ell j+i)}}, $$ where $r$ is a primitive root mod $n$. For particular $n$, one can verify by brute-force arithmetic, carried out geometrically, that a suitable $r$ is a primitive root. The quantities $eta^{(2^ell,n)}_i$, and the relations they satisfy, correspond to provable geometric properties of the regular $n$-gon. (All the properties we need can be translated into integer arithmetic mod $n$, which can be done geometrically.) For example, the relations $eta^{(2,n)}_0+eta^{(2,n)}_1=-1$, $eta^{(2,n)}_0eta^{(2,n)}_1=-2^{k-2}$ follow, geometrically, from the property that $omega$ satisfies $x^{n-1}+x^{n-2}+ldots+x+1=0$. Together these relations imply that $eta^{(2,n)}_0$ and $eta^{(2,n)}_1$ satisfy a quadratic equation that can be solved constructively.

In the case $n=17=2^4+1$, the process is repeated: the quantities $eta^{(4,17)}_0$ and $eta^{(4,17)}_2$ satisfy the relations $eta^{(4,17)}_0+eta^{(4,17)}_2=eta^{(2,17)}_0$ and $eta^{(4,17)}_0eta^{(4,17)}_2=-1$, both of which are provable by brute-force arithmetic translatable into geometry. As before, these relations imply that $eta^{(4,17)}_0$ and $eta^{(4,17)}_2$ satisfy a quadratic equation, expressible in terms of constructible lengths, that can, in turn, be solved constructively. The same can be done for $eta^{(4,17)}_1$ and $eta^{(4,17)}_3$, which satisfy $eta^{(4,17)}_1+eta^{(4,17)}_3=eta^{(2,17)}_1$ and $eta^{(4,17)}_1eta^{(4,17)}_3=-1$.

A third iteration of the idea gives $eta^{(8,17)}_0+eta^{(8,17)}_4=eta^{(4,17)}_0$ and $eta^{(8,17)}_0eta^{(8,17)}_4=eta^{(4,17)}_1$, which imply a quadratic equation in terms of constructible lengths satisfied by $eta^{(8,17)}_0$ and $eta^{(8,17)}_4$, which can then be solved. Once $eta^{(8,17)}_0$ has been constructed, we're nearly done since $eta^{(8,17)}_0=2cos(2pi/17)$.

To summarize, given the regular $17$-gon, one can construct the lengths $eta^{(2^ell,17)}_i$ and prove all needed properties geometrically. Conversely, given the lengths $eta^{(2ell,17)}_i$ for all $1le ellle3$ and $0le i<2^ell$, which Gauss's method constructs, one can construct the points $omega$, $omega^2$, ..., $omega^{16}$, and hence the regular $17$-gon.

Of course this is not a nice proof, since there's a lot of brute-force translation of arithmetic into geometry. (The construction itself is far simpler than the proof that the construction has the desired properties.) The proof (and also the construction) can be streamlined, but I don't see anything in the foregoing that requires the use of axioms beyond those of Euclid.