Alexander van der Vekens: > I think we had such a discussion before, see > https://groups.google.com/d/topic/metamath/F7OY1YoGwFM/discussion
Thanks! I'd searched for it but couldn't find it. On Mon, 13 Jul 2020 14:12:40 -0700 (PDT), Norman Megill <[email protected]> wrote: > 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. ... > 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. Sure, but that's a one-time check in set.mm. I think the better argument *against* prime markings is one you made earlier (my thanks to Alexander van der Vekens for finding the discussion) - namely, can we distinguish ` from ' or whatever the prime marking is? But in most fonts these are relatively easy to distinguish; it's already important to distinguish them in other contexts (such as programming). > 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. ... 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. A lot of the geometry proofs *are* of this form, though, where you have corresponding points. Schwabhauser is full of prime markings. It may very be that it's only when we hit geometry that they become more useful. We could add them there, if that's the consensus. > 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. I think we should keep the convention of "A is class, a is setvar, ph is a wff". I'm just proposing that A' be a class variable just like A is, so there's no big new rule; they just need to learn that "you can use primed variable names". That would be unsurprising; primed names are already very common in mathematics. --- 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/E1jv8le-0002QL-VD%40rmmprod06.runbox.
