I think that a way to represent the parameters of a function when there are more than 2 parameters is to use a
Words of definite length. (Mario Carneiro didn't select this proposal but a word of identified length has its merits.
Here, in the case of parameters for instance.)
You may have:
( f e. ( RR Words 4 ) |-> ( ( f ` 1 ) + ( f `2 ) ) * ( ( f ` 3 ) + ( f `4 ) ) )
You might also use predicates to express a String.
String 4 RR CC + Intvl = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , Intvl >. }
String 5 RR CC + Intvl (/) = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , + >. , <. 5 , (/) >. }
(The 4 and 5 here are to distinguish two constructs. I have not checked if it is possible in Metamath. If not
we can say String4, String5 up to 9.)
The "String" construct is definitely shorter. It is very useful in logic for instance.
We can also consider the first element of a String contains the size of the string
String 4 RR CC + Intvl = { <. 0 , 4 >. , <. 1 , RR >. , <. 2 , CC >. } u. { <. 3 , + >. } , { <. 4 , Intvl >. }
Then the siae may be retrieved by a function that uses the string as its parameter.
I know that Norm doesn't like predicates. For three reasons:
1) Other proof systems don't use class variables. And compatibility is then not insured.
It is a very good reason indeed. Especially because Mario will be annoyed by this in his
work of translation. Right.
2) Set theory, as suggested by its name is about sets. Everything in mathematics can be expressed by sets.
(Seems a philosophical matter for me.)
3) We need to add theorems of the hb* form when we use. (It is true.)
But I also think we need a construct like strings.
For instance if you need to express the concept of betweenness in Euclid's planar geometry, to say
that B is between A and C either you write B e. ( A btw C ) or (other solution) <. <. A , B >. , C >. >. e. btw
But I think the easiest and more readable solution is something like String 3 A B C e. btw. Obviously if you
don't want to be annoyed by the meaning of the symbol String you can replace this symbol by a innocuous one:
¤ for instance: ¤ 3 A B C e. btw.
The first construct is not possible, one is at the level of syntax parsing while the other is an interpretation of a class variable. Is "String N" a valid class? What about "String N A"?
The first construct is not possible, one is at the level of syntax parsing while the other is an interpretation of a class variable. Is "String N" a valid class? What about "String N A"?
We would have:
cs4 $a class String 4 A B C D $.
cs5 $a class String 5 A B C D E $.
It is unambiguous. I've not checked if Meramarh allows that.
> I would put it this way: there are good reasons to use a class predicate instead of a constant,
> but in most cases these reasons are not satisfied. Just make sure that you can explain your reasons.
It is more compact to have String 6 A B C D E F than { <. 1 , A >. , <. 2 , B >. , <. 3 , C >. , <. 4 , D >. , <. 5 , E >. , <. 6 , F >. }. That's my main reason.
And how do you feel about the proposed alternative <" A , B , C , D , E , F "> ?
It looks also good. Except you have additional commas.
Technically yes, but it would be very confusing, because if
String 4 A B C D
is a valid class, then people would generally expect also
String ( 2 + 2 ) A B C D
to be valid, but it wouldn't.
It looks also good. Except you have additional commas.
It looks good but it is not a function. You can't write "( f` ` 3 ) * ( f ` 4 )" if f is a list of parameters to a function.
You need to extract the parameters with a lot of "E.", "dom" and "cod". It is the main drawback.
It is a function. In fact, it is a (Word`S).
The additional commas are not necessarily a bad thing; especially if you get a long run of constants it can get very confusing, e.g.
String 4 1 <_ 4 2
If you are considering this as a way to define structures,
--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
Hi Mario,
> I just pushed a commit a7935db which defines string literals of length up to 8.
Thank you.
> df-s2 $a |- <" A B "> = ( <" A "> concat <" B "> ) $.
You should also replace concat by something short: +c or something like that so that we can write
unobstrusive strings like <" /\c phc psc "> +c <" \/c "> +c <" /\c chc thc "> (obviously with more that
three elements each time).
> [ Replacing ( Words ` X ) ]
No need in fact. As Norm says: if we take set theory seriously, only sets are needed.
I think he really wants that: few constructs with class variables and *only* sets.
The use of a construct with class variables in <" ... "> is only intended to have a natural and readable
representation not to have have actual parameters that would be proper classes.
As for proper classes in <" ... ">, I set it up so that <" A "> = <" ( _I ` A ) ">, which seems to yield the best behavior. Using { <. 0 , A >. } directly causes <" A B C">. to not be a function or have holes in its domain if one of the arguments is a proper class.
> It simplifies a lot of string theorems, eliminating all sethood hypotheses for S except for theorems like
> ( S e. _V <-> Word S e. _V ).
Yes but it weakens the set-theoretic prophylactic wall. It is not a good thing. And we are accustomed to check our
parameters in so many cases that we can do that once more.
As for proper classes in <" ... ">, I set it up so that <" A "> = <" ( _I ` A ) ">, which seems to yield the best behavior. Using { <. 0 , A >. } directly causes <" A B C">. to not be a function or have holes in its domain if one of the arguments is a proper class.
Don't use proper classes that's all. If everything is a set, you don't need to.