Thanks a lot for your remarks. Below my comments: On Saturday, October 19, 2019 at 6:11:36 PM UTC+2, Benoit wrote: > > Not an answer, but a few remarks: > > * The need for more than 26 variables may be a symptom of another problem > than notation. Can you give an example of a statement where you need them ? > The number of available variables is not the problem (within a single theorem). I try to use the same variable for the same concept for related theorems, and that is currently difficult.
> > * A common habit in math is to name variables with primes or indices, e.g. > A' , A'' , A0 (displayed $A_0$), A1 etc. Looks like someone already did > that (see us2.metamath.org/mpeuni/mmascii.html). > Great, I didn't notice that there is already an approach in my intended direction. We should proceed with this, as David also proposed. I thought about maring the alternative variables by a bar above the letter, but primes or indices will also do. Considering primes, however, I am afraid that they can be confused with the accent grave used for function values, e.g. ( F' ` x' ). > > * You write you prefer lower case to denote terms which are always sets, > but I prefer to use the above "decorations" (primes and indices) to stay > closer to other class variables. And also: there is a confusion which was > encouraged by the choice of words "set / class" for the types. I insisted > to change this, and now it is " setvar / class" (already better, but I had > proposed "var / class" to really stop this confusion). The real > distinction is "variable versus term" (in Mario's metamath 0, this is "pure > versus strict"). > I completely agree. > > * Finally, I see in your mm-comments "Usually used for representing a..." > but this is not enforceable and I think it is illusory to want future > contributors (human or computer ones) to use $M$ for a matrix or $P$ for a > polynomial, etc. > Maybe we should not prescribe/restrict the usage at the place where the new variables are defined, but we can provide conventions which variables to use for which concept for a special topic, e.g. "If ` A = ( N Mat R ) ` is the algebra of N x N matrices over (a ring) ` R ` and ` B = ( Base ` A ) ` is its base set (i.e. the set of all N x N matrices over ` R ` ), then special N x N matrix over ` R ` (i.e. elements of ` B ` ) should be denoted by `M ` , ` M' ` , ` M" ` , ` M0 ` or ` M1' `. > > Benoit > -- 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/ffb190fb-9f09-43a5-a04b-bb43611a3f47%40googlegroups.com.
