More formally express the axioms of hyperbolic geometry

axiomshyperbolic-geometrynotation

I have copied word-for-word the axioms (minus the last one which is too long) for hyperbolic geometry as written in Cellular Automata in Hyperbolic Spaces, Volume I: Theory.

Axioms of Incidence

  1. Two distinct points always determine a line.
  2. Any two distinct points of a line determine this line uniquely.
  3. Every line has at least 2 points. There are at least 3 points not lying on the same line.

Axioms of Order

  1. If A, B, C are points of a line and B lies between A and C, then B also lies between A and C, then B also lies between C and A. Write ABC or CBA.
  2. If A and C are two points on a line, then there is at least one point B lying between A and C and at least one point D so situated that C lies between A and D.
  3. Of any three points situated on a line, there is always one and only one which lies between the two others.
  4. Let A, B, C be three points not lying in the same line and let l be a line lying in the plane ABC and not passing through any of the points A, B, C. If l passes through a point of the segment AB, it also passes through either point of the segment AC or a point of the segment BC.

Axioms of Congruence

  1. Consider a segment $AB$ and a point $P$. On every line passing through $P$, it is possible to find at least two points $Q$ and $R$ such that $P$ is between $Q$ and $R$ and such that the segment $AB$ is congruent to each of the segments $PQ$ and $PR$. Write $AB = PQ$ and $AB = PR$.
  2. $PQ$ = $AB$ and $RS = AB$ imply $PQ = RS$.
  3. If $B$ is a point of the segment $AC$ and $B'$ is a point of the segment $A'C'$ and $AB = A'B'$ and $BC = B'C'$, then $AC = A'C'$.
  4. Let $(h, k)$ be a given angle and let $\alpha$ be one of the two half-planes define by a line $a$. Then there is exactly one ray k' issued from $A$ such that $(h, k) = (h', k')$ and such that a point of $k'$ is in the half-plane $\alpha$.
  5. $(h, k) = (h, k)$. Any angle is congruent to itself.
  6. …

How do you write this "more formally"? By that I mean, how do you write it in a more structured way, such as for Coq, or using only logic symbols? I would like to translate this into a custom programming language DSL, but I am currently am far away because these are written in such natural language. I would like to start at a more structured form and them go from there if possible. Knowing how it might be more structured in its presentation will help me in the future be able to translate "naturally written" axioms into a more structured form.

If it's not possible, can you explain why it's not possible, and what is the best we can do?

I have started with this one:

Two distinct points always determine a line.

In programming, I would probably do this by creating a validation function that says essentially $$Line(A, B) \rightarrow True$$ (any two points is a line is basically saying check these two points and say "it's a line").

Then I try:

Any two distinct points of a line determine this line uniquely.

I don't know. I don't see a straightforward way how I'd do this in programming, which is why I'm wondering how you might do it in Coq or in pure Logic symbols. Then I can go from there.

Some of them are somewhat straightforward I think:

If 𝐵 is a point of the segment $𝐴𝐶$ and $𝐵′$ is a point of the segment $𝐴′𝐶′$ and $𝐴𝐵=𝐴′𝐵′$ and $𝐵𝐶=𝐵′𝐶′$, then $𝐴𝐶=𝐴′𝐶′$.

$$(Point(B, AC) \land Point(B', A'C') \land AB=A'B' \land BC=B'C') \rightarrow AC=A'C'$$

Some I think I can get a decent start to, but then I don't know how to represent the finer details:

Of any three points situated on a line, there is always one and only one which lies between the two others.

So I start with something like:

given a, type: Point
given b, type: Point
given c, type: Point
given l, type: Line(a, b, c)
let x = select any (a, b, c)

But not sure how to do the "of any" and "one and only one lies between" parts, especially in logic notation.

Perhaps this will help future self.

Best Answer

When you speak about writing this “more formally”, I get the impression you want predicate logic.

Your example of Line(A, B) → True is not terribly compelling: A predicate that will always be true does not add value to the system. Let's start at the beginning, and focus on your section titles. The first major title is axioms of incidence. So what is incidence? It's a point lying on a line, so you probably want to express this in terms of at least these three predicates:

  • Point(P) is a predicate indicating that P is a point.
  • Line(l) likewise a predicate indicating that l is a line.
  • Incidence(P, l) is a binary predicate, indicating that point P lies on line l.

Depending on your formal system, you might prefer to use set notation, e.g. write P ∈ Points or some such. Or you might want to add some type (or sort) assumptions:

  • ¬ ∃x (Point(x) ∧ Line(x)): No x is both point and line at the same time.
  • ∀P ∀l (Incidence(P, l) → (Point(P) ∧ Line(l))): If there is an incidence, then the first argument is a point and the second is a line.

Now you can start expressing your axioms.

  1. Two distinct points always determine a line.

Better formulation: For every pair of distinct points, there exists a line incident with both of them.

∀A ∀B ((Point(A) ∧ Point(B) ∧ (A ≠ B)) → ∃l (Incidence(A, l) ∧ Incidence(B, l)))

  1. Any two distinct points of a line determine this line uniquely.

If two distinct points are incident with two lines, those two lines must in fact be one and the same. Concluding identity is a standard way for expressing uniqueness in such systems.

∀A ∀B ∀g ∀h ((Incidence(A, g) ∧ Incidence(A, h) ∧ Incidence(B, g) ∧ Incidence(B, h) ∧ (A ≠ B)) → (g = h))

  1. Every line has at least 2 points.

For every line there exist at least two distinct points incident with it.

∀l (Line(l) → ∃A ∃B (Incidence(A, l) ∧ Incidence(B, l) ∧ (A ≠ B))

There are at least 3 points not lying on the same line.

There are three points for which there exists no line incident with all three of them.

∃A ∃B ∃C (Point(A) ∧ Point(B) ∧ Point(C) ∧ ¬ ∃l (Incidence(A, l) ∧ Incidence(B, l) ∧ Incidence(C, l)))

For the second section you probably want to introduce a ternary predicate for order (or “between-ness”). Three points being ordered implies that they are incident with a single line, which helps tie this to the incidence axioms. So I'd go with

  • Order(A, B, C) is a ternary predicate indicating that B lies between A and C.
  • Order(A, B, C) → ∃l (Incidence(A, l) ∧ Incidence(B, l) ∧ Incidence(C, l)) is an axiom asserting that three ordered points are collinear.

Of any three points situated on a line, there is always one and only one which lies between the two others.

Picking this specific example, I'd recommend writing this out in fairly verbose text which you can then turn into formulas. Without any “exactly one” notation as part of typical predicate logic notation, what you do instead is to write down all the cases, each time noting that one of them holds but the others don't.

For any three distinct points A, B, C, if there exists a line incident with all of them, then (A is between B and C and B is not between A and C and C is not between A and B) or (B is between A and C and ...) or (...).

∀A ∀B ∀C (((A ≠ B) ∧ (A ≠ C) ∧ (B ≠ C) ∧
           ∃l (Incidence(A, l) ∧ Incidence(B, l) ∧ Incidence(C, l)))
          → (( Order(B, A, C) ∧ ¬Order(A, B, C) ∧ ¬Order(A, C, B)) ∨
             (¬Order(B, A, C) ∧  Order(A, B, C) ∧ ¬Order(A, C, B)) ∨
             (¬Order(B, A, C) ∧ ¬Order(A, B, C) ∧  Order(A, C, B))))

The third section introduces a lot of new terms: congruence of distances, congruence of angles, incidence between a point and a segment, half-plane, ray. At least the first two make sense to introduce as predicates of your logic. The others you might avoid by using the existing terminology, for example point incident with segment is the same as point lying between the endpoints of the segment. You might still introduce some of them as abbreviations.

Note that the axioms you quoted are common to both Euclidean and hyperbolic geometry. The differences would only come later, in the part that you omitted. So you can probably look at existing formalizations of Euclidean geometry (which should be more common) for inspiration, and then tweak them once you reach the point where things become different.

Related Question