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.
