On Saturday, April 25, 2020 at 1:33:20 PM UTC-4, Jim Kingdon wrote: > > With respect to exclusive or, there are a lot of theorems in set.mm which > use ?? <-> -. ?? (examples: sotric , posn , nneo , nltpnft ). At least some > of these can be productively thought of as exclusive or and may benefit > from notating them as exclusive or. In set.mm this is presumably just a > matter of style or preference. In iset.mm exclusive or is not equivalent > to ?? <-> -. ?? and it may be that some of these theorems naturally > intuitionize to exclusive or. The main example so far is > http://us.metamath.org/mpeuni/rpneg.html intuitionizing to > http://us.metamath.org/ileuni/rpnegap.html but I suspect there might be > others where exclusive or would be the natural intuitionization. >
We need to be a little careful here to see whether this makes the theorem easier or harder to use and read. For example, the proof of ~ cnpart uses ~ rpneg and applies ~ con2bid then ~ df-nel to transform A e. RR+ <-> -. -u A e. RR+ into the equivalence -u A e. RR+ <-> A e/ RR+. Is this easier to do using the xor version? We don't have the large library of theorems for xor that's already been developed for <-> and even <-> -. . So there might be extra conversions back and forth between <-> and xor. Another advantage of <-> is that it can be part of a long chain of equivalences. There is also the human aspect of whether xor makes it easier to understand. First, xor isn't even defined in most math books, so already there is an unfamiliar symbol to some that needs to be looked up. Second, I naturally read ?? <-> -. ?? as "?? if and only if -. ??" i.e. the two sides are equivalent and imply each other. Thinking of it as "either one side or the other side is true but not both" doesn't seem to convey the same meaning. I'm not that used to working with xor and would probably translate it in my head to the <-> -. version (in classical set.mm anyway). Norm -- 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/ec281f59-b8fd-4634-8333-43a2dcccca09%40googlegroups.com.
