Constructibility of the $17$-gon Comment: I greatly shortened and simplified the question. As a drawback, some comments/answers might not make any sense anymore.

Assume we are using this set of axioms $A$ for plane euclidean geometry and some sensible definition of the length $\overline{ab}$ between two points $a$ and $b$. Then we can define the set $R$ to be a regular $n$-gon iff

*

*$R = \{x_j \mid j \in \mathbb{Z}_n \}$ (has $n$ elements)

*$\forall k \in \mathbb{Z}_n : ~\overline{x_{k-1}x_{k}} = \overline{x_{k}x_{k+1}}$ (is equilateral)

*$\forall k \in \mathbb{Z}_n: \angle ~x_{k-1}x_{k}x_{k+1} = \angle~ x_{k}x_{k+1}x_{k+2} $ (is equiangular)

Now imagine someone simply presented you the following construction of a $17$-gon, with an instruction of what he did. The construction yields $17$ points of interest you collect in a set $R$.

Can you prove (or is there a known proof) by only using the Axioms of $A$, that $R$ is a regular $17$-gon?


Comment: The linked construction is one by Herbert William Richmond which I found here, but my question would be the same for any other known construction which does the same job. The origins of the construction are of algebraic nature. Independantly of the origin, I want to know if the answer to my question is positiv, negative or not known.
 A: 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.
