Constructibility of the regular 17-gon [closed]

There is a standard construction of a regular heptadecagon by H.W. Richmond (1893) (https://en.wikipedia.org/wiki/Heptadecagon ) (As anyone knows, it was Gauss who found out that it is possible to do this with a ruler and a compass. It is worth to be noted that he was 19 at the time and that this discovery was among the reasons why he has chosen mathematics rather then languages for a career.) For the sake of clarity, here is the diagram.

The construction works because (or if)

$$\angle AOP_3=\frac{3}{17}\cdot 2\pi.$$

Now, three questions.

Q1. Is it possible to prove this statement using Hilbert's axioms?

Q2. Is it possible to prove this statement using Tarski's axioms? (https://en.wikipedia.org/wiki/Tarski%27s_axioms)

Q3. What the proof, if written in the style of Euclid, may be like?

A few comments. First, it almost certainly does not matter which construction is chosen, but some choice it better to be made here. Second, first two questions are, in fact, reference requests. (Nobody doubts that the answer is yes.) Finally, the last question is about history of mathematics. (Not an alternative history where the construction were discovered by ancient geometers, but the real one.) Invention of algebraic methods made possible nice proofs in place of cumbersome ones, and one may be curious about how much advantage it gives in comparison to the ancient geometric algebra.

closed as unclear what you're asking by Neil Strickland, Mark Sapir, Yemon Choi, j.c., Gerald EdgarJul 10 '18 at 0:26

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• I think Euclid would say (something along the lines of) "Where did you get that glowing box?" Since he could verify the steps and the lengths, he would likely say (something along the lines of) "That's great? Have they trisected the angle yet?" Gerhard "Yes, 'Lines' Is A Pun" Paseman, 2018.07.09. – Gerhard Paseman Jul 9 '18 at 16:05
• One has a fiddly but definite algorithmic construction, and it would be boring but straightforward to write a Euclidean proof. What is to doubt? (The purely algebraic part of it is significant in providing an upper, not a lower, bound on the set of $n$ for which an $n$-gon is constructible.) – LSpice Jul 9 '18 at 16:07
• Did Euclid know that an angle trisector would let you construct a regular heptagon? – Noam D. Elkies Jul 9 '18 at 17:26
• I think OP raises a valid question (though perhaps not research-level): can the proof of the validity of this-or-that construction of the regular $17$-gon attained using modern algebra be translated in Euclid's axioms? I don't think it is obvious, but it is a consequence of theorem 5.1 of arxiv.org/abs/0810.4315 (Avigad, Dean & Mumma, A formal system for Euclid's Elements), which states that every statement true in every ordered field closed under positive square roots is provable in Euclid's Elements. – Gro-Tsen Jul 10 '18 at 0:48
• Jim Conant--see "heptadecagon" in wikipedia for a construction going back to 1893. I think the story you're thinking of is that of the regular 65537-gon---supposedly an advisor, trying to get rid of a student, told him to provide the geometric construction--and he did. – paul Monsky Jul 10 '18 at 1:58

I don't really understand the question. If you can construct a triangle $T$ with angles $2\pi/17, 16\pi/17, 16\pi/17$ you can construct a regular $17$-gon. If you can construct $\cos \pi/17$ you can construct one half of $T$ and hence the whole $T.$ What part of this would escape Euclid?
• The way I understand OP's question, the problem is not the distinction between $\cos(2\pi/17)$ and the regular heptadecagon, the problem is whether the proof that this-or-that construction of either using modern algebra (and manipulations of square roots) can be translated in Euclid's axioms. See my comment on the question and the reference to Avigad, Dean & Mumma's result. – Gro-Tsen Jul 10 '18 at 0:54