Interior and exterior of a polygon in Hilbert axioms

Question

I can't prove one theorem from Hilbert's "Foundations of Geometry". Here is the quote:

Theorem 6. Every simple polygon, whose vertices all lie in a plane $\alpha$, divides the points of this plane, not belonging to the broken line constituting the sides of the polygon, into two regions, an interior and an exterior, having the following properties: If $A$ is a point of the interior region (interior point) and $B$ a point of the exterior region (exterior point), then any broken line joining $A$ and $B$ must have at least one point in common with the polygon. If, on the other hand, $A$, $A'$ are two points of the interior and $B$, $B'$ two points of the exterior region, then there are always broken lines to be found joining $A$ with $A'$ and $B$ with $B'$ without having a point in common with the polygon. There exist straight lines in the plane $\alpha$ which lie entirely outside of the given polygon, but there are none which lie entirely within it.

This theorem can be proved with Hilbert's axioms of connection and order. No need to use congruence, parallel or continuity axioms.

Hilbert writes this theorem may be obtained without serious difficulty with the aid of this theorem:

Theorem 5. Every straight line $a$, which lies in a plane $\alpha$, divides the remaining points of this plane into two regions having the following properties: Every point $A$ of the one region determines with each point $B$ of the other region a segment $AB$ containing a point of the straight line $a$. On the other hand, any two points $A$, $A'$ of the same region determine a segment $AA'$ containing no point of $a$.

but for me it's not so obvious.

I had a few ideas to prove it but none of them was successful. I tried to indicate these regions as a sum of intersections of families of some half-planes and its complement. I also tried to show that a binary relation defined this way:

$A\sim B \iff$ there exists a broken line joining $A$ and $B$ which has no point in common with the polygon

is an equivalence relation with exacly two equivalence classes. I also tried to do this using induction. Can you help me?

Answer 1

This theorem is known under the name of the "polygonal version of Jordan Curve Theorem". In the first editions of The foundations of geometry, Hilbert was saying that the theorem is trivial but he removed this remark in latter editions.

Tom Hales, has formalized the full Jordan curve theorem (https://en.wikipedia.org/wiki/Jordan_curve_theorem), he says that the simple polygonal version is trivial (http://mizar.org/trybulec65/4.pdf):

"Jordan did not write out a proof for polygons, but then again, the proof for polygons is widely regarded as completely trivial. For example, the book What is Mathematics “presupposes only knowledge that a good high school course could impart,” and yet it presents two different proofs of the polygon case of the Jordan curve theorem. The second of these proofs is sketched in eight lines, with “the details of this proof is left as an exercise”"

However, recently, Phil Scott and Jacques Fleuriot described exactly what you are looking for: the full formal proof in the context of Hilbert's axioms (without congruence, parallel, nor continuity axioms). Their proof is computer checked using the HOL-Light proof assistant.

This work is described in the article by Phil Scott and Jacques Fleuriot, Compass-free navigation of mazes, SCSS 2016 (The 7th International Symposium on Symbolic Computation in Software Science). The paper is not online yet, but should be available soon.

Answer 2

I should mention that our SCSS paper only presents a part of the proof, namely the business of finding polygonal paths round simple polygons. This is the most fun part, IMO.

For Hilbert's full theorem, the first written proof attempt is, I believe, by Oswald Veblen, who also usually takes credit for the first rigorous proof of the full Jordan Curve Theorem. Veblen was working with axioms equivalent to Hilbert's, and went on to prove the full Jordan Curve Theorem by adding a completeness axiom. However, his proof of the polygonal case is invalid. In my doctoral thesis, I pinpoint where it goes wrong, and show how a simple adaptation fixes it whilst sticking to the spirit of the proof.

As Julien mentions, the whole proof has been formally verified in HOL Light.