tgsss1, tgsss2, and tgsss3 are not SSS as intended

[david-a-wheeler]

Theorems tgsss1, tgsss2, and tgsss3 are true, but I don't think they prove what was intended.

The comment currently describing theorem tgsss1 says it is "Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of [Schwabhauser] p. 109.". However, tgsss1 does NOT prove that given congruent segments you end up with ABC is-congruent-as-a-triangle with DEF. I would expect SSS to show that 2 triangles are congruent, and tgsss1 doesn't do that. It instead proves that ABC is-congruent-as-an-angle with DEF. That is, tgsss1 proves <" A B C "> ( cgrA G ) <" D E F ">, but I think it's supposed to instead prove<" A B C "> ( cgrG G ) <" D E F "> (note the use of cgrG instead of cgrA).

By using the Google lens app on Schwabhauser, I've become convinced that Schwabhauser also means to use cgrG and not cgrA for theorem 11.51.

I think we should keep these Metamath theorems (renaming them & changing their comment to match what they prove), but I think we separately need the intended SSS theorems from 11.51 that prove that certain triangles are congruent.

Am I misunderstanding something? @tirix @jkingdon @digama0 ?

[tirix]

Thanks for reviewing @david-a-wheeler ! That's very precious. There are indeed two kinds of congruence, and what's important here is actually the notation, more than the explanations in german:

• In chapter 4.4, p35, Schwabhäuser first introduces (length) congruence of a set of points, and in particular for triangles, and chooses to write it e.g. (abc) ≡ (def) (note the parens). I've used cgrG to denote this in set.mm.

  

• In chapter 11.2, p95, Schwabhäuser then introduces angle congruence for triangles, and chooses to write it abc ≡ def without parens . There is actually a special mention in the german text underlining that the lack of parens makes the difference with length congruence introduced in chapter 4.4. I've used cgrA to denote this in set.mm (where the "A" stands for angle).

  

In the statement of the third congruence theorem SSS, the congruence is written without parens, therefore it shall refer to the second kind of congruence, angle congruence. Compare this to the statement of tgsss1

Note that congruence of each of the 3 segments of the triangle is actually the definition of "length" congruence of the two triangles, so if that type of congruence was meant in SSS, it would have been a trivial theorem (c.f. the utility theorem trgcgr which is basically the application of the definition for the case of triangles)

(pinging @avekens and @wlammen as they are the native speakers here!)

[david-a-wheeler]

Ahhh!! I understand, and you're right about the notation. I probably knew this when I plowed through the book a while back, but it's a been a while. The Schwabhauser book is often amazing, but I'm not a fan of this specific notational choice - I think it's way too confusing.

This all seems confusing to me though. For example, the current set.mm text says: "Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent." I agree with this definition of SSS, but that's not strictly speaking what the theorem proves. The theorem as written provides that certain angles are congruent, not that the two triangles are congruent. SSS is widely used (with that definition) in high school textbooks. I think we should have an "SSS" that directly proves ABC is-triangle-congruent-to DEF. It's okay to mention in this reimplementation of 11.51 that its source calls this SSS, but a Google search on "Geometry SSS congruence" finds theorems that show that 2 triangles are congruent, not statements about specific sides.

[avekens]

I think both of David and Thierry are right in a certain extend, and there are in fact some unclear/unprecise statements in Schwabhauser's book. The reason for the misunderstandings are, from my point of view, the lack of a (formal) definition of "the congruence of triangles". In 11.48, there seems to be an informal definition:

Two triangles are congruent if "the six determining properties (sides and angles) of the first triangle and the corresponding properties of the second triangle are congruent"

(in German: Zwei Dreiecke sind kongruent, wenn "... die sechs "Bestimmungsstücke" (Seiten und Innenwinkel) des ersten Dreieckes zu den entsprechenden Bestimmungsstücken des zweiten Dreieckes kongruent sind, ...").

This means the theorems about (triangle) congruence show that from three of the determining properties the remaining three can be derived. With this background information, Schwabhauser's third congruence theorem makes sense: 3 sides are given, and the three angles can be derived from it.

Unfortunately, there is no textual comment by Schwabhauser for this theorem (even in the introduction 11.48 it is not mentioned), and there is no "proof" at all, only the remark "Aus 11.3 ergibt sich sofort 11.51 ..." ("11.51 follows immediately from 11.3").

With this interpretation in mind, I propose to change the comment of ~tgsss1 as follows:

"If the three pairs of sides of two triangles are equal in length, then the three pairs of corresponding angles of the two triangles are also congruent (i.e., equal in size). Hence, the triangles are congruent."

By the way, here are two minor mistakes which might be corrected in this context:

• bewteen -> between
• ~iscgra: definition 11.3 of [Schwabhauser] p. 95. -> definition 11.2 of [Schwabhauser] p. 95.

[avekens]

Maybe a reference to ~trgcgrg could be added to the comment of ~tgsss1, to make clear that ~trgcgrg represents the usual "rule" SSS.

[avekens]

By the way, the three theorems ~tgsss1, ~tgsss2 and ~tgsss3 are not used in set.mm (yet) - what is their intention (except to be a formalization of Schwabhäuser's specification)? Where/how are they used in Schwabhäuser's book?

[avekens]

There is another issue with the Tarski geometry which I dedected:

We currently have two (or looking at the mathboxes even more) definitions of Euclidean spaces (as extensible structures): EEhil and EEG. I tried to prove that they are equivalent, in the sense of having identical entries in the common slots:

    rrxeengbasdisteq.s $e |- S = ( EEhil ` N ) $.
    rrxeengbasdisteq.g $e |- G = ( EEG ` N ) $.
    $( The base sets and the distance functions for the generalized real
       Euclidean space and the Euclidean geometry of the same dimenmsion ` N `
       are equal.  The base set is `( EE ` N )` in both cases.  $)
    rrxeengbasdisteq $p |- ( N e. NN -> ( ( Base ` S ) = ( Base ` G ) 
                                          /\ ( dist ` S ) = ( dist ` G ) ) ) $=

Whereas there are no problems with the base, the distances are different! For S = ( EEhil ` N ), we have

( sqrt ` sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) )

but for G = ( EEG ` N ) we have

sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 )

i.e., the sqrt is missing. I think the definition df-eeng should be adapted accordingly:

    df-eeng $a |- EEG = ( n e. NN |-> ( {
        <. ( Base ` ndx ) , ( EE ` n ) >. ,
        <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |->
            ( sqrt ` sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) ) >. } u. {
        ...
        ) $.

This would be the correct Euclidean distance function.

There should be no impact on the relationship with the congruence relation ~ecgrtg, because the square root is missing on both sides of ( A .- B ) = ( C .- D ), so that it can be eliminated.

[tirix]

There is another issue with the Tarski geometry which I dedected:

We currently have two (or looking at the mathboxes even more) definitions of Euclidean spaces (as extensible structures): EEhil and EEG.

This is not directly related and maybe we could discuss it in a different issue.

Anyway: Initially Scott Fenton defined the class ( EE ` N ) for an Euclidean space of dimension N, and a function Cgr for congruence in EE. In his definition df-cgr, what counts is whether two distances are equal or not, so the square root has been simplified.

Similarly when I introduced EEG what counts in terms of geometry is whether the distances are equal, I guess this is why I missed the square root - that's a mistake, thanks for pointing it out!

Anyway, I think EEhil is a much better option to define Euclidean spaces. As you note, by rrxds, its distance is correctly defined. The development plan here was to show in the general case that all Hilbert spaces can be extended to Tarski Geometries using toTG - that would be the commented out cmodtrkgb, then apply this general result for two special cases:

• the case of the complex plane CCfld,
• the case of Euclidean spaces EEhil.

This would be the program of MPE's chapter 15.4, and means repeating Scott's proofs in a more general setting, up to Tarski's axioms for geometries. ...we are not quite there yet, but once we reach that point, it shall be possible to retire EEG and the related theorems and to replace it by ( toTG ` ( EEhil ` N ) )

[jkingdon]

Initially Scott Fenton defined the class ( EE ` N ) for an Euclidean space of dimension N, and a function Cgr for congruence in EE. In his definition df-cgr, what counts is whether two distances are equal or not, so the square root has been simplified.

To me it is odd to have a distance function at all in formalizing Tarski's geometry axioms. I realize we justify this by saying We intentionally choose to represent congruence (without loss of generality) as 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 instead of "Congr 𝑥𝑦𝑧𝑡", as it is more convenient. but at least in my mind that feels like assuming what we are trying to prove. We 'know" that the axioms taken as a whole make this representation acceptable but we can't use metamath itself to justify that.

Now, I haven't been much involved with formalizing geometry in set.mm and I'm not sure I will dive into it, so I will defer to those who are doing work on it about what, if anything, to do about this.

[tirix]

That's a very valid point (but also yet a different issue? ;-) ). Initially it was Mario's suggestion to define it this way, and indeed it requires a justification outside of Metamath to admit that our definition indeed corresponds to what is meant.

[digama0]

You can prove it in metamath too, if you formalize geometry with a 4-ary relation you can show that there exists a distance function satisfying the rules. It's not that complicated: you map <x, y> to its equivalence class with respect to the relation <x, y> Congr <z, w>. IIRC the equivalence relation axioms are all given directly in Tarski's axioms so this is not a particularly big leap IMO.

[jkingdon]

That's a very valid point (but also yet a different issue?

Oh definitely a different issue, as this is a tangent off of a tangent.

[david-a-wheeler]

I'm going to post in this comment about my original question/issue involving congruence.

First, I agree with @avekens that the comment for tgsss1 be modified to:

"If the three pairs of sides of two triangles are equal in length, then the three pairs of corresponding angles of the two triangles are also congruent (i.e., equal in size). Hence, the triangles are congruent."

However, I think there's a broader problem. The definition of "congruence" used by Schwabhäuser (and thus currently in set.mm), while defensible, is different from the definition used in all other texts I know of. We have two definitions of congruence so far:

• In chapter 4.4, p35, Schwabhäuser first introduces (length) congruence of a set of points, and in particular for triangles, and chooses to write it e.g. (abc) ≡ (def) (note the parens). In set.mm @tirix chose to use cgrG to denote this kind of congruence. I'll call this "corresponding length congruence".
• In chapter 11.2, p95, Schwabhäuser introduces angle congruence for triangles, and chooses to write it abc ≡ def without parens (the lack of parens makes a difference). In set.mm @tirix chose to use cgrA to denote this in set.mm (where the "A" stands for angle). I'll call this "angle congruence".

However, every geometry text I've seen uses a different definition for triangle (or shape) congruence: "all corresponding lengths and all corresponding angles are congruent". I'll call this definition "full congruence", and we don't currently have any particular notation for it. This is really odd, because a vast amount of high school geometry involves "prove that 2 triangle are congruent, then use CPCTC to show that the parts you cared about are congruent." E.g., https://mathresearch.utsa.edu/wiki/index.php?title=Triangle_Congruence

Would it make sense to have a definition of "full congruence" in set.mm to meaning that "all corresponding lengths and angles are congruence"? There's no difference between "full congruence" and "corresponding length congruence" in Euclidean geometry - is there a Tarski geometry where there is a difference? If there is, I think we should at least create such a definition. Even if we don't create a separate definition of "full congruence", we probably ought to make this distinction clearer in the comments since many will presume we mean one thing when we say congruence, but we really mean another. For example, we should say "corresponding length congruence" or similar instead of simply "congruence" in places where cgrG is used, since that's all that is directly asserted by it.

[david-a-wheeler]

On the tangent about distances (because I guess it's okay to have tangents in geometry)...

I agree with Mario that representing congruences as equal distances is a good representation. While it's not strictly necessary, a lot of geometries have distances, so representing them this way makes them much easier to build on. Mario said:

You can prove it in metamath too, if you formalize geometry with a 4-ary relation you can show that there exists a distance function satisfying the rules....

I'd love to see that proof in set.mm, as it would formally justify this representation.

[tirix]

Would it make sense to have a definition of "full congruence" in set.mm to meaning that "all corresponding lengths and angles are congruence"?

I think "modern day" geometry has only two definitions:

• Congruence indeed stands for (length) congruence
• Similarity is what is used for "angle congruence"

I think we should stick to just those two concepts, but we could add as a precision to the definition of angle congruence df-cgra that it is usually called similarity in geometry classes (and why not add the Wikipedia link).

You can prove it in metamath too, if you formalize geometry with a 4-ary relation you can show that there exists a distance function satisfying the rules....

I'd love to see that proof in set.mm, as it would formally justify this representation.

I believe we could prove that fact completely outside of geometry, by showing that given a function F Fn A, these two partitions of A are the same:

• the set of preimages by F, ( `' F ` { d } ) for d e. ran F
• the quotient set ( A /. R ) for the relation R defined by x R y <-> ( F ` x ) = ( F ` y ).

And that conversely, given a relation R, one can define a function F with that property. A choice function (mapping all elements S e. A to a chosen representative of its equivalence class [ S ] R) who do the trick.

In our geometry application, A is the set of couple of points in the space( P X. P ), F is the dist function, and the corresponding R relation is the congruence relation.

[tirix]

We could prove the following theorem in the first direction:

|- ( F Fn A -> E. r ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) )

And the converse:

|- ( R Er A -> E. f ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) )

[david-a-wheeler]

I think "modern day" geometry has only two definitions: Congruence indeed stands for (length) congruence

Not so. I've never seen that definition used in high school geoemtry at least (and I have a number of such textbooks). Without exception every definition of triangle congruence uses the different definition given in Congruence shown in Wikipedia:

Two triangles are congruent if their corresponding sides are equal in length, and their corresponding angles are equal in measure.

Note that having equal sides is not the definition of triangle congruence, that's only half of it. Every book I've seen is careful to distinguish "sides are congruent" with "triangles are congruent", and in particular, once you prove the first (sides are cogruent), then as a separate step you can prove that the triangles are congruent. The whole point of "SSS" is to convert "sides are congruent" to "triangles are congruent", which doesn't make sense if you can't distinguish those statements.

Which means that under the current definitions in set.mm it is not possible to accurately state the proofs in a typical high school textbook.

I realize it's a little odd, but I think in this specific case it would make sense to add two more definitions:

• "All angles are congruent" (cgrAA or something like that) - we can easily build on cgrA do this this. This will make certain similarity statements easy to make.
• "Shapes are fully congruent", (cgrF or similar), that is, all sides AND all angles are congruent. We can build on cgrG and cgrAA to do this.

The "fully congruent" one, in particular, would let us accurately capture claims and results. I realize we try to be sparing about creating new definitions, but full congruence is a really basic and universal concept in geometry; we should have a way to directly and easily represent it. What's more, it would be easy to create given the current definitions. In Euclidean geometry cgrG and cgrF are true for the same triangles, but they have different meanings, and we should be able to precisely capture those differences in meaning. While we sometimes create variations from standard terminology, there's no reason for us to do so in this case.

[tirix]

Indeed I did not scroll down to the triangle congruence, since the definitions in set.mm are for a (finite) set of points - thanks for noticing.

I understand your arguments, but still I believe our preference to limit the number of new concepts introduced should have precedence here. I don't think there is any other instance in set.mm where we have two completely equivalent definitions. I would instead prefer to add explanations in the comments for the definition or the related section, and links to theorems that prove the different properties (for example, that congruence implies similarity). I'd be interested to hear more opinions (@digama0 @jkingdon @avekens @benjub ?).

For reference, a few more definitions:

• PlanetMath's congruence
• WolframWorld's congruence
• WolframWorld's similarity

Note that all those definitions of congruence use isometries and compositions of isometries. Schwabhaeuser also introduces the concept of isometry, it would be interesting to show that when two shapes are congruent, there is a motion (an isometry of the entire plane) transforming one into the other. The converse is valid by definition, so we have an equivalent definition of congruence based on isometries.

[avekens]

As I mentioned before, Schwabhäuser defines the congruence of two triangles only informally. But his informal definition corresponds exactly to the CPCTC principle. To formalize this, let A, B, C, D, E, F e. P be 6 points and T = { A , B , C } and R = { D, E , F } two triangles. Then we could define the congruence of two triangles T and R by:

T ~ R :<-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) 
/\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\  <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) )

which is equivalent (using the definition of cgrG) to

T ~ R :<-> ( <" A B C "> ( cgrG ` G ) <" D E F "> 
/\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\  <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) )

That means the 6 corresponding parts (3 sides and 3 angles) are congruent iff the two triangles are congruent.

With this definition, the "rule" SSS could be written as

<" A B C "> ( cgrG ` G ) <" D E F "> -> T ~ R

which can be proven easily by ~tgsss1, ~tgsss2 and ~tgsss3.

I think that we do not need such a definition in set.mm, but we can use it in the comments to explain the differences of the involved concepts.

[tirix]

What we do have a lot in set.mm are alternative definitions, proven as theorems, and oftentimes the alternative definitions are actually the textbook definitions. I'm thinking about, for example, dfbi2, dfdif2, dfss2...dfss6, to name only a few of the more than a hundred currently in set.mm. For example, dfpr2 is actually a textbook definition of an unordered pair.

I would suggest we introduce a theorem like:

dfcgrg2 $p |- ( <" A B C "> ( cgrG ` G ) <" D E F ">  <-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) 
/\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\  <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) $=

which states that congruence for two triangles can also be defined as congruence of each segment and each angle (6 parts), and which can be derived from the definition and tgsss1, tgsss2, and tgsss3. We can add in this theorem's comments that this is the actual textbook definition of triangle congruence, and provide links to references.

[benjub]

I don't have much time to dwell on the discussion here, but in my opinion @tirix has (and has had, when he designed that whole set.mm section) the good point of view, which strikes a balance between the elementary expositions and the set.mm practices.

[avekens]

I would suggest we introduce a theorem like:

dfcgrg2 $p |- ( <" A B C "> ( cgrG ` G ) <" D E F ">  <-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) 
/\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\  <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) $=

which states that congruence for two triangles can also be defined as congruence of each segment and each angle (6 parts), and which can be derived from the definition and tgsss1, tgsss2, and tgsss3. We can add in this theorem's comments that this is the actual textbook definition of triangle congruence, and provide links to references.

That is really a good idea and should be a possibility to harmonize the conflicting opinions within this discussion. @david-a-wheeler do you agree?

[digama0]

FWIW I agree with @tirix 's characterization, we deliberately avoid multiple provably-equal definitions in favor of multiple definitional theorems. We also favor short definitions, so that would suggest keeping SSS as the definition and SSSAAA as the theorem.

[david-a-wheeler]

Aa @tirix notes:

What we do have a lot in set.mm are alternative definitions, proven as theorems, and oftentimes the alternative definitions are actually the textbook definitions... I would suggest we introduce a theorem like: dfcgrg2 $p |- ( <" A B C "> ( cgrG ` G ) <" D E F "> <-> ... which states that congruence for two triangles can also be defined as congruence of each segment and each angle...

Great point. Ok, we should do that, and make sure that the comments explain the rationale for using "all correlating distances are the sane" as triangle congruence.

However, does this really cover all cases of shape congruence when the shapes are a set of connected points? According to: https://en.wikipedia.org/wiki/Congruence_(geometry) :

congruence may be defined intuitively thus: two mappings of figures onto one Cartesian coordinate system are congruent if and only if, for any two points in the first mapping, the Euclidean distance between them is equal to the Euclidean distance between the corresponding points in the second mapping.

... but is that true for other Tarski geometries, even if non-Euclidean? If it is, then perfect, let's prove that as well (probably building on the triangle congruence proof). If not, then maybe we need something else defined as well.

(I will not be very available for the next few days, so please excuse any delays.)

[tirix]

I think this issue can be closed as fixed by #2994 (and @jkingdon 's comment addressed by #3014)

[david-a-wheeler]

I think we need to tweak the documentation so readers can easily see explanations and jump from one part to another, and then we can call this closed. I'll create a proposed pull request to try to do that.