Proposal: Allow primed class variables in set.mm body (e.g., A')

[David A. Wheeler]

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

[ookami]

Hello David,

(1) How do you expect this to be clearly distinctive from df-fv? (2) There are numerous write styles in use for all kind of mathematical classes, e.g. I've seen German Fraktur for topological spaces. I think your proposal opens up a can of worms,in the end, once an exception is tolerated.

I am not sure whether your idea really works this way. One should implement a translator that produces adapted output on the web sites only, to accomodate to common styles in particular fields of mathematics.

Wolf

[fl]

> 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!) 

Very clearly I propose that we reactivate what I had done on the geometry of Euclid using 

Wayne Aitken's handouts. It's in English. It's very easily formalizable. All the preliminary 

definitions have already been entered. There's very rich material with Euclidean and 

non-Euclidean geometry. 

We can put that in the history section. And we can go on to formalize Euclid itself. 

And we can add links to Oliver Byrne's work because his proofs are very easy to understand 

and can help to understand the formalized version if we take care to stay close to the text.

https://www.c82.net/euclid/

It won't compete with Schwabauser's version. The latter will be the official geometry

in the main section. And the Euclid/Aitken version will be in a historical section.

We will thus have a section that will follow the rules of the historical sections in that 

its purpose will be to be as close to Euclid as possible in order to be an aid to reading the Elements.

And moreover David will not have to break his head to decipher a German text.

Finally, being able to compare Schwabauser's and Euclid's versions will enrich both versions.

-- 

FL

 

[David A. Wheeler]

On Sun, 12 Jul 2020 14:24:34 -0700 (PDT), "'ookami' via Metamath" <meta...@googlegroups.com> wrote:
> (1) How do you expect this to be clearly distinctive from df-fv?

The usual way, by their rotation.

df-fv uses backquote, that is: `
Primes in set.mm currently use straight quote, that is: '
Many programming languages already depend on people being
able to see the difference.

If it's desired we could make prime markings
more distinctive in Unicode by using
U+2032 (HTML Entity &#8242; aka &#x2032; aka &prime;).
Here's a compare & contrast:
ASCII: ( F ` A' )
Unicode: ( F ` A′ )

> (2) There
> are numerous write styles in use for all kind of mathematical classes, e.g.
> I've seen German Fraktur for topological spaces. I think your proposal
> opens up a can of worms,in the end, once an exception is tolerated.

No worms, just more support for a widely-used symbology.

The problem is that it's not obvious if A and E have some sort of correspondence,
but it's obvious that A and A' are intended to have some sort of correspondence.

> I am not sure whether your idea really works this way. One should implement
> a translator that produces adapted output on the web sites only, to
> accomodate to common styles in particular fields of mathematics.

I have no idea how to implement a translator that could figure out,
ahead of time, that A and E have a correspondence in a particular theorem.
Nor should we do so, because that would create an undesirable distance
between the actual set.mm proof and its display.

It's better to use names to hint to the reader the class purpose.
We already do this throughout set.mm; "P" means the "set of points"
for example in the Elementary Geometry section. But only having A through Z
means that every class seems to be unrelated to each other; the lack
of prime notation makes it impossible to hint to the reader about
correspondences in a way that is typically done in math texts.

--- David A. Wheeler

[ookami]

> No worms, just more support for a widely-used symbology.

> The problem is that it's not obvious if A and E have some sort of correspondence,
> but it's obvious that A and A' are intended to have some sort of correspondence.

The problem is that this kind of symbology arises in other fields as well. I personally, for example, find relations difficult to read in Metamath, especially when they are chained. One can easily argue along your lines that a different font for differentl set types improves readability - and I agree, it would! Or enclosing subexpressions in parentheses could be relaxed by prioritizing operators. And, and, and... . Your idea is just one out of a plethora of typographical aids to point out the semantics of formulas. Thats why I speak of a can of worms.

> I have no idea how to implement a translator that could figure out,
> ahead of time, that A and E have a correspondence in a particular theorem.
> Nor should we do so, because that would create an undesirable distance

> between the actual set.mm proof and its display.

There is no simple solution to this problem. My first idea is that a processor evaluates a tag like comment with hints on how to display otherwise difficult to read math expressions. This has to be written from scratch. Improving readability is just a task completely different from proofs, and can/should be solved separately.

Wolf

[David A. Wheeler]

On Sun, 12 Jul 2020 16:05:30 -0700 (PDT), "'ookami' via Metamath" <meta...@googlegroups.com> wrote:
> ... Your idea is just one

> out of a plethora of typographical aids to point out the semantics of

> formulas. ...

The fact that there are other ideas doesn't make it a bad idea.
This idea doesn't conflict with other ideas, either.

So let's focus on the merits of the actual proposal.

> My first idea is that a
> processor evaluates a tag like comment with hints on how to display
> otherwise difficult to read math expressions. This has to be written from

> scratch. ...

Feel free to write a new typographic system from scratch! That will take a lot of work.

What I propose requires 0 changes to all Metamath-processing programs.
It doesn't even require adding new lines to set.mm, as they're already in a mathbox;
they simply need to be moved into the body. That makes my proposal
*quite* different from a proposal to rewrite a typography system from scratch.
It can be done today with a minor tweak to set.mm - and you're done.

Even if someone creates a new typography system,
having class variable names like A' available will mean
that the typography system can immediately take advantage of it,
instead of trying to reason those relationships out itself.

Rewriting a completely different typography system is essentially
unrelated to supporting variable names like A'. You can do either, both, or neither.

I'm hoping that there will be agreement to supporting A' and friends;
it's a trivial change with some simple benefits.

--- David A. Wheeler

[Stanislas Polu]

I second the A' proposal. Anecdotally, when working with synthetic
proof generators, we've multiple times been relying on the existence
of the primed class variables (despite these being defined in
mathboxes).

-stan

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jumT6-0002Gj-HR%40rmmprod06.runbox.

[ookami]

So far any variable has been a one-letter entity from distinct alphabets (for what it was worth).  If you think about giving up this principle, I think one is better off using indexed variables across all types of variables(logic expression, set and class). The idea is (if I understand right) to group variables showing a common relationship. Then I think this should go beyond pairs, and include tripletts, quartetts and so on.

Wolf

[Alexander van der Vekens]

I think we had such a discussion before, see https://groups.google.com/d/topic/metamath/F7OY1YoGwFM/discussion

I was in need of additional variables (which could have been also primed ones), but Mario and Norm convinced me that there may be risks. Please have a look at their arguments in the referenced discussion.

Alexander

[Norman Megill]

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

[David A. Wheeler]

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 <n...@alum.mit.edu> 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