Thank you, Norm, for this background information. I see the risk of a
misuse of additional variables, and I also had concerns about using the
primes ', " (which can be confused with the grave accent grave ` ).
My initial intend was to use special variables for special cases.
One of these cases (replacing a setvar variable in a definition by a class
variable in a corresponding theorem) is described in my initial posting: `
def $e |- I = ( p e. L |-> V ) $. ` , ` defval $p |- ( ( ph /\ .p. e. L )
-> ( I ` .p. ) = ... ` . If P is not used elsewhere, it can be used instead
of .p., but if it is already used, it is a littel bit strange to use P' in
this case: ` defval $p |- ( ( ph /\ P' e. L ) -> ( I ` P' ) = ... ` .
Another case would be the need for class variables of the same kind, e.g.
"Let ` M e. ( Base `` A ) `and ` M' e. ( Base `` A ) ` be two matrices ...
". Here, the "prime" solution is adequate, but could cause the difficulties
explained by Norm.
A third case is the usage of setvar variables in antecedents/hypotheses,
see, for example, ~ gsumcom3:
gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) )
Here, j and k should be replaced by J and K or, if J and K are already in
use, by J' and K'. I often thought that there is a theorem which could help
me proving my theorem, until I find out that it requires setvar variables
in its hypotheses, but in my case there is a class expression at this place
- I have to revise/reprove the concerned theorem, or I have to perform a
transfomation of the class (expression) into a setvar. Maybe it is not a
good idea to allow free setvar variables in hypotheses/antecedents at all,
because these could always cause such problems. But this is a different
topic.
As a concrete example, in which I am running out of adequate available
variables, are theorems about matrices having polynomials as entries. For
these theorems, I use the following capitel letters as class variables with
fixed meaning (in addition I also use symbols-as-class-variables for
certain operations):
- ` R ` : represents a ring.
- ` B = ( Base `` R ) ` is its base set
- ` P = ( Poly1 `` R ) ` is the polynomial algebra over (the ring) ` R `
- ` K = ( Base `` P ) ` is its base set
- ` Y = ( var1 `` R ) ` is its variable
- ` E = ( .g `` ( mulGrp `` P ) ) ` is its exponentiation
- ` A = ( N Mat R ) ` is the algebra of N x N matrices over (the ring) `
R `.
- ` M = ( Base `` A ) ` is its base set
- ` C = ( N Mat P ) ` is the algebra of N x N matrices over (the
polynomial ring) ` P `.
- ` D = ( Base `` C ) ` is its base set
- ` Q = ( Poly1 `` A ) ` is the polynomial algebra over (the matrix
ring) ` A `.
- ` L = ( Base `` Q ) ` is its base set
- ` X = ( var1 `` A ) ` is its variable
- Z: Zero (if .0. is already used)
- O: One ( if .1. is already used)
- T: Transformation (e.g. of a matrix consisting of polynomials into a
polynomial with matrix coefficients)
- F: diverse auxiliary mappings
- I,J: integers (indices, sum variables, etc)
That means only 7 letters are remaining: CGHSUVW. Usually, V and W are used
for arbitrary classes, indicating that certain classes are sets (e.g. ` ( X
e. V -> ... ) `), so only 5 capital letters are actually remaining: CGHSU.
This means there is no large choice for concrete objects like matrices and
polynomials to be represented.
Maybe a mechanism for local class variables (only visible/usable within the
scope in which they are defined) could be helpful, but this would be a too
heavy conceptual change of the metamath system, at least for the moment.
As a conclusion, I would propose *not *to provide additional class
variables in general at the moment. As a first step, it may be helpful to
provide a table listing all class variables (including the
symbols-as-class-variables) and explainig for which mathematical concept
they are used commonly/frequently. We can put this table into section
"convention", adding the advice to use the shown variables for the
indicated concept whenever possible/adequate. My list shown above could be
a part of such a table...
--
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/932d1eca-c399-4dd2-bc31-145c79e478b4%40googlegroups.com.
