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.
On April 25, 2020 8:22:03 AM PDT, Benoit <[email protected]> wrote: >1) I do not have strong opinions for concatenation: either "concat", >which >is self-explanatory, or "++", which might be a bit more obscure, is >good >(better than the other alternatives). > >2) As for symmetric difference, $\triangle$ is the more standard >notation, >with a nice ascii version being "/_\". Also, since XOR is in Main, >then >symmetric difference could be moved to Main too, in my opinion. > >3) Regarding logical connectives, I agree with Norm that >and/or/implies/iff/not/true/false are sufficient. It is also nice to >have >XOR, NAND as examples, even though they are not used outside of >propcalc. >It would be nice to have a subsection with NOR which parallels that for > >NAND. No need for "negated implies", "(negated) is implied by", and >(negated) projections. > >Benoît > >-- >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/7bf244ec-854e-4ec5-834b-12a219a5c442%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/DE56DD17-CC3C-48C9-80E3-F50CC9067052%40panix.com.
