Sometimes things that may seem useful in a local context may be problematic in the bigger picture. In addition to the posts Alexander pointed to, let me elaborate some of my thoughts.
In trying to keep things as simple as possible, we have generally resisted adding things to set.mm (such as multiple definitions for the essentially the same concept) that, while perhaps slightly (and arguably) more friendly from a human point of view, do not add anything essential to the formal mathematics. Primed variables are a gray area we have avoided so far. In books and papers, I don't always like decorated variations of the same variable. Maybe the worst for me are numeric subscripts on variables, like p_1 through p_3 for a figure with 3 points (where the 1,2,3 are just arbitrary subscripts that have nothing to do with an ordered sequence). They are harder to read, it takes longer to write expressions by hand, and it is easy to make mistakes transcribing the subscripts in a complicated expression. More than once I've relabeled them p,q,r before working out details on paper. One disadvantage of primed variables is that you may need to determine from context that they are just a decoration and not a function. If you're studying a book from the beginning, this isn't a problem, but if you are just quickly looking up a specific result, you may have to go back and verify that a primed variable is just another variable and not, say, a derivative or orthocomplement. Older geometry books often used primed variables, but I thought it was interesting that the 9th grade geometry book that I helped my nephew with last year didn't have any primed variables as I recall. Two triangles, even if congruent, were labeled with different letters like ABC and DEF. I don't know the reason, but maybe the authors' thinking was that priming a variable might be confusing for a beginner, especially since other decorations usually represent concepts derived from or based on the variable e.g. <A (angle A) means the angle at triangle vertex A. Also, outside of definitions of things like congruent triangles, it was rare that you'd have 2 triangles in complete isolation; instead you'd usually be working with subtriangles of a more complex figure, say ABC and ABD with a common point or side, where priming some of the variables wouldn't make much sense. Several colorblind people have told me they find it hard to determine visually that a letter or symbol is a variable on the web pages where we distinguish them with color. So in order to make them independent of the web page color, we have adopted the convention of using lower case italic for setvar letters, upper case italic for class variable letters, and dotted underlines for symbols used as class variables. (That was one reason I switched some symbols like "_V" and "_i" to be Roman about 10 years ago, even though in some books they are italic.) Primed variables would add another complication to the mix. In any case, if the overwhelming consensus is that people really want them, I would suggest baby steps: move only those primed variables you feel a compelling need for to your mathbox, at the time you add the theorem, so we can get a sense of the look and feel of the proofs and decide whether it makes sense to import the primed variables for general use. Norm On Sunday, July 12, 2020 at 4:03:28 PM UTC-4, David A. Wheeler wrote: > > I propose that we allow A' , B' , etc., as class variables, at least to > support geometry. > This would make it much easier to indicate corresponding values (such as > points) > and make it easier for proofs to more obviously match their original > source material. > Having primed variables is already common mathematical practice, so we'd > be > supporting common practices. > > Background: > I'm hoping to contribute to the Elementary Geometry section, so I've been > walking through > the current set.mm work due mostly to Thierry Arnoux, Mario Carneiro, and > Scott Fenton. > This involves reading [Schwabauser], something of a trick since it's in > German and > I can't read German. (Hello Google translate!) > > An unnecessary challenge in doing this is that the geometry proofs > often involve many points that correspond to each other, which is > typically indicated by > a prime. However, the set.mm main body doesn't support that. This > inability to easily indicate > point correspondences makes it unnecessarily hard to read the proof > statements, AND > it creates an unnecessary difference between set.mm and the original > source material. > > For example, here are the key hypotheses and conclusion of > http://us.metamath.org/mpeuni/tgifscgr.html > > π΅ β (π΄πΌπΆ) ; "B is between A and C" > πΉ β (πΈπΌπΎ)) > (π΄ β πΆ) = (πΈ β πΎ) > (π΅ β πΆ) = (πΉ β πΎ) > (π΄ β π·) = (πΈ β π») > (πΆ β π·) = (πΎ β π») > Proves > (π΅ β π·) = (πΉ β π») > > If we allowed A' etc., this could expressed as the following, which > is MUCH clearer because the "primed" class variables make > correspondences MUCH more obvious: > > π΅ β (π΄πΌπΆ) ; "B is between A and C" > π΅' β (π΄' πΌ πΆ' ) > (π΄ β πΆ) = (π΄' β πΆ' ) > (π΅ β πΆ) = (π΅' β πΆ' ) > (π΄ β π·) = (π΄' β π·' ) > (πΆ β π·) = (πΆ' β π·' ) > Proves > (π΅ β π·) = (π΅' β π·') > > Having "primed" variables is very common in mathematics, and > there's no technical reason set.mm can't support them. > These are *already* defined in the Mathbox for Jonathan Ben-Naim, so they > just have to be moved up. We could also move up double-primed (A") if > desired. > > Let's do it! > > --- David A. Wheeler > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fe0bac85-d673-4f37-bf8b-75e067e8d4feo%40googlegroups.com.
