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 [email protected] schrieb am Montag, 13. Juli 2020 um 10:13:14 UTC+2: > 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 > > On Mon, Jul 13, 2020 at 2:37 AM David A. Wheeler <[email protected]> > wrote: > > > > On Sun, 12 Jul 2020 16:05:30 -0700 (PDT), "'ookami' via Metamath" < > [email protected]> 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 > > > > -- > > 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/E1jumT6-0002Gj-HR%40rmmprod06.runbox > . > -- 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/40c1261a-efd2-4f2a-ad9a-56d22367b3aen%40googlegroups.com.
