Around Hilbert's theorem: the center of a circle is not constructible by straightedge alone

TL;DR

This paper rigorously proves Hilbert's theorem regarding the non-constructibility of a circle's center with straightedge alone, extending models of Euclidean constructions and analyzing classical proofs.

Contribution

It formalizes and extends models of Euclidean constructions, providing rigorous proofs of Hilbert's theorem and its variants, including for the projective plane.

Findings

Proves the impossibility of constructing the center of a circle with straightedge alone.

Constructs points from nothing using compass and straightedge with arbitrary points.

Analyzes and clarifies issues in classical proofs of Hilbert's theorem.

Abstract

In order to state the theorem in the title formally and to review its rigorous proof, we extend and make more precise the Uspenskiy-Shen-Akopyan-Fedorov model of Euclidean constructions with arbitrary points; we also introduce formalizations for infinite configurations and for the projective plane. We exemplify the proof method by simpler and not so well known results that it is impossible to construct the unit length, or a given point, by compass and straightedge from nothing by means of classical arbitrary points. On the other hand we construct any given point by compass and straightedge from nothing by means of arbitrary points determined by horizontal segments. We quote a "proof" of Hilbert's theorem from the literature and explain why it is problematic. We rigorously prove Hilbert's theorem and present three variants of it, the last one for the projective plane.