> 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 guess what got me down this whole line of thinking was the text "A positive integer is even or odd but not both" from the comment to http://us.metamath.org/mpeuni/nneo.html But all the points about "one more symbol to worry about, make convenience theorems for, etc" are certainly valid. And even in iset.mm it is a bit unknown at this point whether recasting some of these theorems with xor will make things easier. I've done a few experiments in that direction, and it might have helped with a situation or two which can be and is solved differently in set.mm. But this is early days in terms of trying out this technique. I'll endorse the recommendation of caution. On April 25, 2020 1:36:08 PM PDT, Norman Megill <[email protected]> wrote: >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. -- 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/006246BC-0834-488B-97E2-5AD7F619A7DF%40panix.com.
