Geometry: Hilbert's axioms

[Jerry James]

I see that geometry has been discussed in this forum before, and I see some work on geometry in set.mm.  What is the current thinking on this topic?  Is somebody actively working on it?  I would like to do so, and am happy to collaborate with any other interested parties.

I first became interested in theorem provers in graduate school, due to running into several incorrect proofs in papers I reviewed.  Then I came across this book at a library book sale:

<LI><A NAME="Borsuk"></a> [Borsuk] Borsuk, Karol and Szmielew, Wanda,

<I>Foundations of Geometry,</I> North-Holland Publishing Company, Amsterdam,

The Netherlands (1960) [QA681.B633].</LI>

That book piqued my interest in formal proofs, although I was too far along on my dissertation to change directions then.  Still, that book has occupied a place on my shelf all these years.  I think when I first introduced myself in this forum a couple of years ago that I mentioned working on Cutland's book about Universal Register Machines.   I didn't mention that I was also working in parallel (no pun intended) on this book on geometry.  The URM work ground to a halt eventually (that pun was not intended, either), and I've been working solely on the geometry material since.  But I made some bad decisions early on that have negatively affected the later material, and I haven't chosen very good names.  I think I need to start over and do it right this time, and do it in public view to take advantage of the experience of others.

The book referenced above uses a somewhat simplified form of Hilbert's axioms to develop a theory of geometry.  Would that be okay as a basis?  It should be possible to keep it distinct from work based on other sets of axioms through judicious choice of names.

Caveat: I am a software developer by profession, so I can only work on this on evenings and weekends.  If a particular evening or weekend is otherwise occupied, it might take me a day or two to respond to messages.  I am sure this can be annoying.  (Tomorrow night, for example, I have an engagement, so I probably won't reappear until Saturday.)

For those who might have access to a copy of the book, I have proved all but two of the theorems in the first 20 sections of chapter 1, and about half of section 21.  I will list the section names below for those who might be interested.  The two theorems I have not proved are both related to the topology of the line.  I simply don't understand the set.mm material on topology deeply enough yet to prove them; more study for me!

Sections I have worked through, along with a brief description of the definitions added in support of each:

    Introduction: Primitive Notions

       - Basic geometry: a structure whose base set is the points, along with a

         set of lines and a set of planes.  Each line and each plane is a set

 of points.  Incidence is the element-of relation.

       - The class of colinear figures

       - The class of coplanar figures

    1. Axioms of Incidence

       - A class for each axiom of incidence

       - Incidence geometry: the intersection of the basic geometries and the

         axiom classes

    2. Three Non-Collinear Points and Four Non-Coplanar Points

    3. Lines and Planes

       - Operator mapping two distinct points to their unique containing line

       - Function mapping three noncolinear points to their unique containing

         plane

       - Operator mapping a line and a point not on the line to their unique

         containing plane

       - Operator mapping two distinct intersecting lines to their unique

         containing plane

    4. Fundamental Existence Theorems

       - The minimal incidence geometry, containing 4 distinct points, 6

         distinct lines, and 4 distinct planes

    5. Intersections of Lines and Planes

    6. Linear Axioms of Order

       - Slot accessor for the between relation on points, thereby extending

         the basic geometry structure with an additional slot

       - A class for each linear axiom of order

       - Linearly ordered geometry: the intersection of the incidence

         geometries and the axiom classes

    7. Segments and Open Segments

       - Operator mapping two distinct points to the open segment between them

       - Operator mapping two points to the closed segment between them

       - Operator mapping two distinct points to the closed-open segment

         between them

       - Operator mapping two distinct points to the open-closed segment

         between them

       - The class of (linearly) convex figures

    8. Open Segments on a Line

    9. Division of an Open Segment

   10. Common Part of Two Open Segments

   11. Topology on the Line

       - The class of open segments on a line

       - The class of closed segments on a line

   12. Half-Lines

       - Operator mapping a point of origin and a distinct directional point to

         a half-line

       - Operator mapping a point of origin and a distinct directional point to

         the complement of a half-line

       - The class of half-lines

       - Function that maps a half-line to its point of origin

       - Function that maps a half-line to its unique containing line

       - Function that maps a half-line to its complement

       - Function that maps a half-line to its closure

   13. Half-Lines on a Line

       - Operator that maps a line and a point on the line to the pair of

         half-lines lying in the line whose origins are the point

   14. Half-Lines on a Given Half-Line

   15. Orientations of a Line.  Axes.

       - The same-orientation relation on half-lines

       - Function that maps a line to the half-lines contained in the line

       - Function that maps a line to the set of axes on the line

       - The class of axes.  Note that the book distinguishes orientations and

         axes, but I saw no reason to follow suit.  (An orientation is a set of

         half-lines closed under the subclass relation.  An axis is an ordered

         pair: an orientation and its enclosing line.  However, given an

         orientation X, its containing line is uniquely determined: U. X.)  The

         metamath development conflates the two notions.

   16. Order of Points on an Axis

       - Operator that maps an axis and a point in the containing line to the

         unique half-line contained in the axis with that point as its origin

       - Precedes relation on the points of an axis

   17. Betweenness Relation for a Line and Two Points

       - The relation of a line lying between two points

   18. Plane Axiom of Order

       - A class corresponding to the plane axiom of order (a form of Pasch's

         Axiom)

       - Ordered geometry: the intersection of the linear ordered geometries

         and the class corresponding to the plane axiom of order

   19. Half-Planes

       - The same-side-of-a-line relation on points in a plane

       - The class of half-planes

       - Function mapping a half-plane to its containing plane

       - Function mapping a half-plane to its boundary line

       - Function mapping a half-plane to its complement

       - Operator mapping a line and a point not on the line to the unique

         half-plane with the line as its boundary line and containing the point

       - The relation of a line lying between two figures

       - The relation of a plane lying between two points

       - The same-side-of-a-plane relation on points

   20. Pencils and Half-Pencils of Half-Lines

       - Operator mapping a plane and a point in the plane to the pencil

         contained in the plane with the point as its vertex

       - The class of pencils; a pencil is a maximal set of half-lines in a

         plane with a common point of origin

       - Function mapping a pencil to its containing plane

       - Function mapping a pencil to its vertex

       - Operator mapping a pencil and a point in the pencil to the unique

         half-line in the pencil containing that point

       - Operator mapping a half-plane and a point in the boundary of the

         half-plane to the half-pencil contained in the half-plane with the

 point as its vertex

       - The class of half-pencils

       - Function mapping a half-pencil to its vertex

       - Operator mapping a half-pencil and a point in the half-pencil to the

         unique half-line in the half-pencil containing that point

I am currently working on section 21:

    21. Betweenness Relation for Half-Lines

The remaining sections of chapter 1 are:

    22. Ordering of a Half-Pencil

    23. Angles

    24. Characterization of Lines and Planes in Terms of the Betweenness

        Relation

    25. Triangles.  Open Triangles.

    26. The Open Triangle and the Line

    27. Topology on the Plane

    28. Polygonal Lines

    29. Quadrangles

    30. The Intersection Point of the Diagonals of a Quadrangle

    31. Polygons and Their Triangulation

Chapter 2 introduces the axioms of congruence governing the equidistant relation.  Showing the independence of the parallel postulate happens much, much later in the book.

Regards,

-- 

Jerry James

[Jim Kingdon]

If you want geometry axioms, I'm kind of partial to Tarski's: https://en.m.wikipedia.org/wiki/Tarski's_axioms

And if you haven't seen it already,
http://geocoq.github.io/GeoCoq/ is at least worth a glance.

Doing this in set.mm would also be interesting. Although you seem to know more than I do about what is already there.

Oh, and no worries about being a part time contributor. Many of us are.

[savask]

I'm going to advocate for Tarski's axioms as well :-)

They are short, work for higher dimensions and had been used by other proof systems before (such as Coq in GeoCoq and HOL Light in its proof of the independence of the parallel postulate). The big disadvantage is probably that the only book about building geometry from Tarski's axioms is written in German (I'm talking about Schwabhauser, Szmielew, Tarski "Metamathematische Metoden in der Geometrie"). The book is written very formally, so it might be possible to understand it without knowing much German + proofs from GeoCoq may help a lot.

Also, Scott Fenton did some work on Tarski's axioms before, but as was mentioned in https://github.com/metamath/set.mm/issues/49 , technically it's not an axiomatic formalization. Once you fix the presentation of geometry, it must be easy to "recode" his material to use this new structure though.

Finally, one can start from Tarski's axioms and prove Hilbert's axioms from them, as a sort of compromise. For example, see http://www.michaelbeeson.com/research/papers/TarskiProvesHilbert.pdf .

[David A. Wheeler]

I would love to see geometry formalized in metamath set.mm/iset.mm. See the discussion here:
https://github.com/metamath/set.mm/issues/49
https://github.com/metamath/set.mm/issues/52

Mario believes it's very important to use extensible structures to do this, and has some other interesting comments as well. I don't feel confident working out those definitions. I'm hoping that he or someone else could work out some sort of definitions that we could generally agree on, move them to the main body, and then we can all work on together. Here is one comment from him:

> I think that both Aitken's (Hilbert's?) axioms and Tarski's are worth formalizing, preferably in a way which makes it easy to have a structure satisfying both systems so that we can draw parallels (ha!) between them.
> Here's a proposal for Tarski's axioms as an extensible structure: ....

I would love to see progress in this area "unstuck", and I don't know enough about this area to get it resolved.

--- David A.Wheeler

[savask]

I'm not comfortable with making up new definitions for metamath, but how about the following:

df-absgeom $a |- AbsGeom = { g | [. ( Base ` g ) / p ]. [. ( Slot 2 g ) / b ].
   [. ( Slot 3 g ) / c ].
   ( ( ( ( ( ( ( A. x e. p A. y e. p <. x , y >. c <. y , x >.  /\
   A. x e. p A. y e. p A. z e. p A. w e. p A. r e. p A. s e. p
     ( ( <. x , y >. c <. z , w >. /\ <. x , y >. c <. r , s >. ) ->
     <. z , w >. c <. r , s >. ) ) /\
   A. x e. p A. y e. p A. z e. p
     ( <. x , y >. c <. z , z >. -> x = y ) ) /\
   A. x e. p A. y e. p A. z e. p A. w e. p E. q e. p
     ( y b <. x , q >. /\ <. y , q >. c <. z , w >. ) ) /\
   A. x e. p A. y e. p A. z e. p A. u e. p
   A. f e. p A. g e. p A. h e. p A. v e. p
     ( ( ( -. x = y /\ y b <. x , z >. /\ g b <. f , h >. ) /\
     ( ( <. x , y >. c <. f , g >. /\ <. y , z >. c <. g , h >. /\
       <. x , u >. c <. f , v >. ) /\ <. y , u >. c <. g , v >. ) ) ->
         <. z , u >. c <. h , v >. ) ) /\
   A. x e. p A. y e. p ( y b <. x , x >. -> x = y ) ) /\
   A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p
     ( ( u b <. x , z >. /\ v b <. y , z >. ) ->
       E. w e. p ( w b <. u , y >. /\ w b <. v , x >. ) ) ) /\
   E. x e. p E. y e. p E. z e. p
     ( -. y b <. x , z >. /\ -. z b <. y , x >. /\ -. x b <. z , y >.  ) ) } $.

It (I hope) defines absolute geometry with dimension at least two, which roughly corresponds to Tarski_neutral_dimensionless in GeoCoq (see http://geocoq.github.io/GeoCoq/html/GeoCoq.Axioms.tarski_axioms.html). Letter p is the set of points, b is between relation and c is congruence relation.

Then one can define Euclidean/hyperbolic geometry by adding the parallel postulate or its negation; dimension can be specified as another axiom as well.

[Thierry Arnoux]

Attached is something I started around a year ago. Though I did not go
very far, I think this is the direction in which Norm and Mario wanted
to go with geometry.
It shall be very similar with what Alexander just posted.

BR,
_
Thierry

[David A. Wheeler]

Mario and Norm:

Can you confirm that this is the direction you both wanted to go? If this isn't what you wanted, can you provide an alternative definition?

On short: Can you help get us marching in some common direction?


--- David A.Wheeler

[Mario Carneiro]

Thierry's sketch seems like a good way to go about it. It sounds like Jerry has already done quite some work on geometry; is this in metamath and if so how are the initial definitions set up?

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Benoit]

I also think that Tarski's axioms will be easier to implement in metamath, and indeed the GeoCoq and Michael Beeson's websites (and their articles) are nice resources.  I got acquainted with Tarski's geometry reading

Tarski, Alfred; Givant, Steven Tarski's system of geometry. Bull. Symbolic Logic 5 (1999), no. 2, 175–214. (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9012)

Tarski's system also has some modularity, and as savask proposes, one can start with the elementary, neutral, dimension-free part.

I would like to mention also

Makarios, A further simplification of Tarski's axioms of geometry, https://arxiv.org/abs/1306.0066

which removes one axiom from the absolute part, keeping modularity.

There are slight and subtle variations in the formulations of the axioms from one presentation to another, and Makarios's article does a nice job mentioning these caveats (especially regarding independence).

Benoît

[Jerry James]

On Friday, October 5, 2018 at 6:59:43 PM UTC-6, Mario Carneiro wrote:

Thierry's sketch seems like a good way to go about it. It sounds like Jerry has already done quite some work on geometry; is this in metamath and if so how are the initial definitions set up?

Yes, I have been working in metamath.  But I think nobody is going to like the initial definitions I have used.  I think I mentioned that I made some poor choices early on.  You'd better work out what you want those initial definitions to look like, then I'm happy to contribute proofs on top of that.  If you really want to see what I have, I can put it in a git repository.

-- 

Jerry James 

[Mario Carneiro]

Thierry's mm file looks like a starting point. Is there a missing part or non obvious definition that you want us to investigate? If nothing else, your work would make it clear what definitions are needed, and if you release it it might also help others in the future. And that's assuming it is really as bad as you say - if you have found a better approach then that would be even better.

Mario

--

[Jerry James]

Very well.  What I have done so far is in the geometry branch of https://github.com/jamesjer/set.mm.  The branch name is a bit misleading, as I have everything I've tried with metamath all squashed together in there: URMs, geometry, and experimental additions to the main part of set.mm.

If it looks like I tried to write PVS specifications with the metamath language, there's probably a reason for that. :-)

I will look at Thierry's work this week.

[David A. Wheeler]

Excellent, thanks so much. I think we all ought to look at this and the other options, and slowly start working out some sort of agreement on what to do about geometry. We really can't make much progress until there is agreement about some basic constructs and definitions, and I know I do not know enough to work them out.

--- David A.Wheeler

[Thierry Arnoux]

Hi all,

I had a look at Jerry's formalization of geometry and this is an impressive work.

I suppose one way to make use of this work, if we insist on using Tarski's axiomatization, would be to prove Hilbert's axioms from Tarski's axioms.

Am I correct that we now have works with three different geometry axiomatizations?

• Jerry James's work: Hilbert's axiomatization using on extensible structures (Points/Lines/Planes),
  
• Scott Fenton's work: Proof that the Euclidan space of dimension N ' EE ' fulfills Tarki's axioms (Points/Congruence/Betweenness)
• Frédéric's work: Aitken's Incidence-Betweenness geometry using extensible structures (Points/Lines/Betweenness), marked for private use.
  

BR,
_
Thierry

--- David A.Wheeler --

[Jerry James]

Thank you for the kind words, Thierry.  I've been looking at GeoCoq and am quite impressed.  The idea of building from (some version of) Tarski's axioms, but showing the relationships between various sets of axioms (including Hilbert's) is appealing.  Whatever the community decides to do, I would love to be involved.

My copy of the Schwabhauser book arrived in the mail today.  I'm leaving town for a few days, so I will take the book along, as well as a German-English dictionary which I am sure will be completely inadequate.

I haven't had time to look at Makarios's work yet.  I will try to do that when I get back.

Regards, Jerry James.

[Thierry Arnoux]

Hi Jerry,

In any case, I believe your work is worth including in set.mm. 

Maybe we could gather more opinions before moving it in, but as a matter of fact, you’re free to put whatever you want in your mathbox anyway.

Eventually, formalisations of geometry, whatever their axiomatic foundations, will have to show that geometric lines are isomorphic to the real line (RR).  I think this can e.g be achieved by equipping lines with a group structure, with segment concatenation as an operation, showing that this group is ordered and Archimedean, and therefore isomorphic to (a subgroup of) the additive RR, by Hoelder’s theorem (which remains to be proved in set.mm)
BR,

_

Thierry

--