Prove SAS etc. theorems for triangles

[david-a-wheeler]

Now that we have Tarski geometry we can have various theorems such as side-angle-side (SAS).

There are detailed proofs using OTTER and Tarski Geometry here: http://www.michaelbeeson.com/research/FormalTarski/

@tirix @sctfn - I don't know if that's your longer-term aim, but it seems like a plausible direction!

[tirix]

I see four interesting paths to develop elementary geometry:

• to show that “generic” Hilbert spaces fulfill Tarski’s axioms, so that we have even more generic examples of geometries than Euclidean spaces,
• to show that a Tarski geometry fulfills Hilbert’s axioms, (like Beeson did),
• to show that non-Euclidean geometries exist,
• to continue on the path of Schwabhaeuser and build distances and angles on Tarski geometries. (Beeson did that too)

The SAS-like theorems will come from the last branch of development, like many other results of elementary geometry, but right now we are still far from it. It’s like we’re still building on set relations, and have not defined the real line yet.
I believe different people may work independently on different branches, with a minimum of synchronization and cooperation.
There are maybe even other paths to take, like, to do the same starting with a different axiomatisation of geometry.

[tirix]

PS. SAS is chapter 11.49 in [Schwabhaeuser], the other triangle congruence theorems are the next chapters 11.50, 11.51.

[david-a-wheeler]

Unfortunately Schwabhaeuser is in German, and I can't read German. Do you know of an English translation?

[benjub]

I think that unfortunately, there is no English translation, but it still is the reference book in this domain. A bit like EGA and SGA are in French and have only partial translations, but are still the reference books for algebraic geometry.

There is a big difference between reading German and reading mathematical German (same with French, English...). I give it to you that it's less convenient and that you miss things in the preface and introductions, but knowing a few dozen words (main verbs, conjunctions and technical vocabulary specific to the book) and the general syntax of the language is enough to get the gist of it. And if I recall correctly, Schwabhaeuser has almost more formulas than text. Good luck !

[tirix]

Commit 26d2f82 / PR #1744 includes a proof for the first congruence theorem (SAS). Three to go! :)

[tirix]

PR #1744 also includes a proof for the third congruence theorem (SSS). Two to go! (but those first two were the easiest..)

[david-a-wheeler]

Very awesome!

For those who are following this issue, I did end up buying Schwabhauser, and I'm using a combination of Google Translate and studying the formula is to understand what the German says. It's a good book, but it's definitely challenging for those who don't read German :-) .

[tirix]

Angle-Side-Angle (ASA) is part of #1767

[tirix]

FYI, @jorge-agra has posted a proof of AAS here: mm-tgaas
That is a separated repository and not a PR in set.mm, hopefully we can get it into set.mm too.
Interestingly, Jorge did not strictly follow [Schwabhaeuser].

[jorge-agra]

Added PR #5432 per @tirix recommendation