What is ++ being used for currently? - (++) is df-symdif, the symmetric difference of sets, defined in Scott Fenton's mathbox. Other than that, I can't find any use of unparenthesized ++ anywhere, so I'm not even sure what the comparison is against. (Note for the future, please quote definitions by their label, not their ascii symbol, as this is better for searchability.)
Mario On Fri, Apr 24, 2020 at 3:25 PM Norman Megill <[email protected]> wrote: > FL asked me to post these. > > > -------- Forwarded Message -------- > Subject: ++ > Date: Fri, 24 Apr 2020 21:33:34 +0200 (CEST) > From: fl > To: Megill Norman > > Hi Norm, > can you post this? > > I suggest that ++ replace concat. Currently ++ is used for a concept > rarely if ever used. On the contrary > concat is very useful and the symbol > is long. ++ is already used for concatenation in some computer languages. > > -- > FL > > > -------- Forwarded Message -------- > Subject: Binary connectors > Date: Fri, 24 Apr 2020 21:48:04 +0200 (CEST) > From: fl > To: Megill Norman > > Hi Norm, > > by the way can you recall to the participants that there are 16 binary > logical connectors and that some are still missing. They are in a logical > mood seemingly. > > -- > FL > > > My comments: > > > 1. I have no strong opinion on ++ vs. concat, except that "concat" seems > more self-explanatory. "concat" occurs 373 times in set.mm, so ++ would > save 1492 bytes in set.mm size. > > > 2. I think it would be pointless and wasteful to add new symbols for all > 16 binary logical connectives. Just having to memorize all of them would > be a pain. > > and/or/implies/bicond, together with unary not, satisfy virtually all > mathematical needs. The rest are trivial variants obtained by adding a > unary not. That is much simpler to become familiar with than 16 separate > symbols and their definitions. Moreover, we would need a very large number > of theorems to convert between the possible combinations and manipulate > them, with no real benefit. > > Even operations common in digital logic, like xor and nand, are rarely > used in ordinary mathematics. Most books on mathematical logic don't even > define them. They are primarily used in some specialized applications like > axiomatics of the Sheffer stroke. > > 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/ca241c3c-ca3b-456c-8dec-e82284509405%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/ca241c3c-ca3b-456c-8dec-e82284509405%40googlegroups.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/CAFXXJSuFBDm%3DOeVE%2Btbyftyzcn3asy%2B5-pN_LRZExyOks5LXOg%40mail.gmail.com.
