Answering Mario's test question: If I see "sum_ k e. A B" and I don't know
the definition, then I will hope that A does not contain occurrences of k
;-) And if it does, then I would tend to think that the occurrences are
bound, simply because k looks "dummy" in "k e. A", so the occurrences in A
should, too. (I admit I don't know if it's the case or not, I would have
to look at the definition.)
Your example of the dependent Pi type is interesting. Do you have a
concrete example where the "indexing set" depends on the index variable,
and where it is important that the occurrence be free?
Your other examples (nlab, bounded Zermelo, many-sorted logic) are very
interesting. They show that we should really avoid using the degenerate
instance of df-opab and instances of df-ral where A contains occurrences of
x, etc. Since you are fine with it, if Norm agrees, I would like, as
proposed in my previous message, to discourage use of df-ral, df-opab,
etc., to deduce from them dfral, etc. which are identical but have a dv
condition, and to use only the latter. Would this help for your
translation project?
I wrote above that Mario's proposal df-opab3 would yield
|- { <. x , x >. | x = 2 } = { z | E. x z = <. x , 2 >. }
and I said that this was clearly false. Mario wrote:
> This is intended behavior. I think we should probably more or less ban
the use of { <. x , x >. | ph }, but when it is used, I want it to have
this behavior; BOTH x's are new bound variables, and they are always bound
in the order written, so the second x shadows the first and hence you can
rename the "outer" one to get { <. x , x >. | x = 2 } = { <. y , x >. | x =
2 }. I think that using { <. x , x >. | ph } to mean a subset of the
diagonal is a horrible hack because it implies a flexibility on the left of
a set comprehension that we don't actually have, and it breaks the pattern.
If you have the general rule "all multiple binders are bound from left to
right" you can guess this behavior without having to read the definition
(assuming you realize that { <. x , y >. | ph } is a syntax constructor in
the first place, rather than the composition of <. x , y >. and a
nonexistent { A | ph }.)
I agree that writing { <. x , x >. | ph } is a hack (albeit not a horrible
one), for the reasons you wrote. The thing is that we write this
informally very often, and everyone understands it as some subset of the
diagonal. Therefore, I agree that we should avoid/discourage or even ban
it, but if this has to be defined, then it should really denote the
intended subset of the diagonal. It looks like on this last point, we have
a deep disagreement, due to our different backgrounds.
I think I understand your points (though I'll certainly reread your posts),
and I see how your proposal would help compatibility with typed languages,
but here is the thing: there is a necessary compromise to find between
proximity to mathematical practice and ease of coding (or "computer
semantics", not sure what the best term is), since these two objectives may
be conflicting sometimes. I think that having, for instance, definitions
which imply that { <. x , x >. | ph } is not a subset of the diagonal,
would be going too far away from mathematical practice.
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/f3990aac-1550-4e12-a3e5-c8b0c4bd4a09%40googlegroups.com.
