I was thinking the same thing, every integer is even or odd is a good example of XOR but I wouldn't recommend it for most uses (and even for nneo we will probably want the iff version because it has more theorems about it).
On Sat, Apr 25, 2020 at 7:39 PM Jim Kingdon <[email protected]> wrote: > > 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/006246BC-0834-488B-97E2-5AD7F619A7DF%40panix.com > <https://groups.google.com/d/msgid/metamath/006246BC-0834-488B-97E2-5AD7F619A7DF%40panix.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStnDx-qtGNxem%2BuZBQ9S%3DzG6C5eeJ7K1s_7-q31hgxt2w%40mail.gmail.com.
