Prove the Independence of the Parallel Postulate (Metamath 100 #12)

[tirix]

This should be easier to formulate after #49 has been done.

[avekens]

Theorems ~eengtrkg ( N e. NN -> ( EEG `` N ) e. TarskiG ) and ~eengtrkge ( N e. NN -> ( EEG `` N ) e. TarskiGE ) are alredy available, contributed by @tirix (see also Issue #49) . That means TarskiG =/= (/) can be shown immediately. So all we need is an example for a class C with C e. TarskiG and C e/ TarskiGE (to show that ( TarskiG \ TarskiGE ) =/= (/). C could be a model (Klein-Beltrami?) of the hyperbolic plain, but we need, as @tirix already mentioned in #49, definitions and theorems for hyperbolic plains. Is anybody working on this topic? Currently, Metamath is number four together with Lean in the "Formalizing 100 Theorems" ranking (http://www.cs.ru.nl/%7Efreek/100/) with 74 proven theorems, so we should get some distance to keep place 4 at least for a while...

[tirix]

We have to be very careful in the choice of the model of hyperbolic geometry, because choosing the wrong model might make proving the Tarski's axiom much more difficult. For one I agree we should limit ourselves to a 2-dimensional model, so e.g. (a subset of) the complex plane could be used.

On a Klein disc, geodesics are easy to define (they are simple euclidean segments), but I'm afraid distance/congruence would be complicated, since it involves finding intersections with the unit circle (that involves solutions of a quadratic equation), and then computing a cross ratio.

I wonder if the hyperboloid model, or even the Gans model would not be easier to work with. In those models, lines are branches of hyperbolae, so they should not be hard to define, but more importantly distances follow a simple bilinear form (we could drop the acosh in the distance formula, since we are only interested in equality of distances).

[avekens]

On a Klein disc, geodesics are easy to define (they are simple euclidean segments), but I'm afraid distance/congruence would be complicated, since it involves finding intersections with the unit circle (that involves solutions of a quadratic equation), and then computing a cross ratio.

I am just about to prove theorems for the intersection of a line with a circle. I hope I can provide them shortly. There will be, however, still a long way to go afterwards to add theorems for the Klein-Beltrami model of the hyperbolic plain.

[benjub]

What about the Poincaré half-plane ? It has some pretty nice properties, although I have not thought them through for the present problem. In any case, it's true that one should "benchmark" them before any lengthy work. Note that there is also the Poincaré disk.

[icecream17]

I'm going to add a definition for projective planes (as part of elliptic curves) Does EEG + line at infinity (the real projective plane or extended Euclidean plane) satisfy C e. TarskiG and C e/ TarskiGE?

https://en.wikipedia.org/wiki/Projective_plane https://ericmoorhouse.org/handouts/projective_planes.pdf

It's not euclidean because there are no parallel lines... I'm pretty sure it satisfies all TarskiG axioms:

• distance axioms: reflexivity (x dist y = y dist x) and identity (x dist y = z dist z -> x = y)

  Consider all triples of reals (a, b, c) but not (0, 0, 0). Reduce by the equivalence (a, b, c) equiv (na, nb, nc) for any n != 0. For example (3, 4, 7) is equivalent to (9, 12, 21). By dividing by a (if a != 0), all points are either equivalent to (1, x, y) or (0, x, y). [The latter case reduces even further to (0, 1, y) or (0, 0, 1). Let's say (0, 1, y) is incident with every line with the gradient (or slope) y, and (0, 0, 1) is incident with every vertical line.]

  Thus this structure is isomorphic to points on the real projective plane: (1, x, y) if the point would be (x, y) on the real Euclidean plane, else (0, x, y) if the point is on the line at infinity.

  The distance between (a, b, c) and (d, e, f) would then be (abs(a - b), sqrt((b-e)^2 + (c-f)^2)), i.e. (0 or 1, Euclidean distance). I just made this distance function up I can't find it anywhere. But it's equivalent to the euclidean distance function when the points at infinity aren't involved, and it satisfies the distance axioms.

• 2nd betweenness axiom by "for any two lines, those lines have an intersection"
• 3rd betweenness: I assume the subsets are all on the same line, so this is true by how regular lines work (I think the segment between a euclidean point and a point at infinity would just be the entire line)
• 5 segment: Probably the most likely to be unsatisfied since I can't verify.
• TarskiG_CB: Any two points has a line, any two lines has a point, so just use y -- v -- (intersection of yv and xz)

[icecream17]

While trying to figure this out, I found https://researchgate.net/publication/266748037_Herbrand's_Theorem_and_Non-Euclidean_Geometry

In the abstract it says "We use Herbrand's theorem to give a new poof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involved constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simpler, and intuitively appealing proof."

This might shorten the process of proving this theorem.

[tirix]

Herbrand's theorem used to give a new poof that Euclid's parallel axiom is not derivable

This is a very interesting paper, even more so because the publishers, Michael Beeson and Julien Narboux both have worked on formalization of Geometry in Coq. It's a really different approach, but it working on the meta-level, and I don't think we have those tools formalized yet...

Projective plane

First of all it's great that you're working on that! I think @benjub already had some theorems about the projective line in his mathbox.

I'm unsure about the 5-segment axiom, but I believe that Euclid's axiom will still hold in the geometry of the projective plane. In order to disprove it, given a point and a line, you'll need to find more than one line containing the point and not intersecting with the line. In projective plane, since all lines intersect at one point, you will not find any non-intersecting line.

[benjub]

For the independence of Euclid's postulate, using the Klein-Beltrami disc see https://researcharchive.vuw.ac.nz/handle/10063/2315

I think the real projective plane is not suitable since it does not yield a model for Tarski's axioms of absolute geometry (which is either euclidean or hyperbolic, but not elliptic). But @tirix may know this better.

As for projective spaces, if you are serious about introducing them, I advise opening a new issue. The very few results about the real and complex projective lines in my mathbox are not suitable: they are designed for the special purpose of having slightly larger number systems (compactifications of R and C), but not with generality in mind. For projective spaces, I advise defining a function taking a vector space as argument. The field of scalars need not be commutative (i.e., a division ring suffices). I don't remember set.mm's conventions regarding this. You may define it for modules, by identifying two nonzero vectors if and only if they are multiple of each other via an invertible element, though this would not give the "correct" notion of projective space in general (you would miss the nonfree submodules).

[icecream17]

Isabelle's proof seems to be less meta: https://www.isa-afp.org/entries/Tarskis_Geometry.html

---

Edit: Naively it seems relatively close to being possible

We probably have already proved a good chunk of all of these except the last two

The links above go directly to the code, and the more readable explanation of some parts is at https://openaccess.wgtn.ac.nz/articles/thesis/A_Mechanical_Verification_of_the_Independence_of_Tarski_s_Euclidean_Axiom/16999462/1?file=31449043