FL: ++; binary connectives

[Norman Megill]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ca241c3c-ca3b-456c-8dec-e82284509405%40googlegroups.com.

[Norman Megill]

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.

I'll also mention that Tarski used a frown symbol for concatenation in his 1965 paper.  His notation is reproduced on p. 190 of the Metamath book, using the LaTeX symbol "\frown".

Norm

[Mario Carneiro]

I like the idea of using ++ for concatenation, particularly in ascii notation, since I don't want to try to reproduce a frown symbol in ascii. I think the most common symbol for this is adjacency though.

Mario

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/009468c4-d9a5-4553-b72c-6811ff0a6e1b%40googlegroups.com.

[David A. Wheeler]

On Fri, 24 Apr 2020 18:50:11 -0700, Mario Carneiro <di....@gmail.com> wrote:
> I like the idea of using ++ for concatenation, particularly in ascii
> notation, since I don't want to try to reproduce a frown symbol in ascii. I
> think the most common symbol for this is adjacency though.

I also have (mild) prefererence for "++" to represent concatenation.
In particular, I'd prefer "++" as the ASCII representation, with a Unicode display
of ⧺ (U+29FA) and \doubleplus in LaTeX (package unicode-math).
This is somewhat common in Computer Science; Haskell uses "++"
for concatenation, and many other programming languages use "+" for concatenation
(but they can use types to figure out what overloaded operation was meant).
I think ++ would make the ASCII display a little simpler, and many people think of
"add" and "concatenate" as related... so having intentionally similar symbols
has some mild advantages.

Frown looks a little like intersection, even though there's no relationship,
and that could be considered a negative for it.
That said, frown has significant use, it's not terribly ambiguous,
and it just works, so I'm not unhappy with it.

Bottom line: I have a minor preference for ++, but it's not a big deal to me.

I agree that "no displayed symbol, just adjacency" is common. However,
generally in Metamath we try to be very explicit, so I think we shouldn't have
"no displayed symbol" in Metamath (at least in set.mm) for concatenation.

Notation is hard. There's a brief related discussion here:
https://math.stackexchange.com/questions/298648/is-there-a-common-symbol-for-concatenating-two-finite-sequences
I don't like the other options discussed there (the other symbols already
have other conflicting meanings), so I think frown and doubleplus are the contenders.

--- David A. Wheeler

[Alexander van der Vekens]

I also like the idea to replace concat by a symbol, and I agree with David that we should decide between frown and doubleplus. As ASCII symbol for frown we could take '^' (only one character more than ++). From a visual point of view, I would prefer the frown (looks like joining the two operands), but I also would be happy with ++. As a compromise: we could take ++ as ASCII symbol and frown as display symbol - but this would be maybe too confusing...

Alexander

[Benoit]

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

[Norman Megill]

From FL:

-------- Forwarded Message --------
Subject: ++, indices and Commons
Date: Sat, 25 Apr 2020 11:53:57 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

could you post this:

Yes I made a mistake. Scott Fenton uses (++) and not ++.  So the symbol ++ is available.

I would also appreciate if the first index of a word is 1not 0. The C language has arrays that begins et 0 and its a pain un the neck because you always have to deal with n - 1 expressions.

I would also recommend that we have a part intermediate between the official one and the sandboxes so that people could mutualize their contributions. We could begin by those related to categories, topology, and words. We could call this part "Commons" by refererence to the fields belonging to the community in England before the XIXth century.

--
FL


My comments:

1. I have no issue with changing "concat" to "++". As for the Unicode symbol, I would lean towards just the simple "++" (two characters) rather than "⧺" (which looks weird to me, almost suggesting "not parallel" rather than 2 plus signs) but I'll go along with whatever people want.

Frown is also acceptable to me (maybe even my personal first choice, given that it may be more common outside of computer science literature), maybe with .^. or ^^ or '` (upside down df-cnv) as the ASCII token.  But if more people prefer ++ that is fine.


2. I assume you mean df-word.  As Mario suggested, it would be helpful if you provide the label of what you are referring to.

I probably agree with you but I haven't worked with df-word, so others' comments would be more valid. I wonder if the awkward "( M ..^ N )" would largely be replaced by "( M ... N )". At this point, though, there are hundreds of theorems involved and probably a huge effort to convert.  An important question is whether the literature typically starts with 0 or 1, which I don't know, and it's nice to be follow the literature convention when possible.

(In C, I often start arrays with 1 because that's the way humans count. For me at least it leads to fewer bugs, and being able to use n instead of n-1 over and over saves typing and might even make up for the wasted memory space of the unused 0th entry. I imagine, though, that for "real" C programmers, counting from 0 is second nature so that when they see index n it mentally means the (n+1)th entry to them, so they don't need to use n-1.)


3. Note that we already have a section called "(Future - to be reviewed and classified)" http://us.metamath.org/mpeuni/mmtheorems.html#dtl:17.3 that was added primarily for the purpose of the "Commons" you mention. If people think that renaming it to "Commons" would be more intuitive, that's fine with me. Maybe "(Commons - to be reviewed and classified eventually)".

Norm

On Saturday, April 25, 2020 at 11:22:04 AM UTC-4, Benoit 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.

I could accept this.
 

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.

Well, I didn't mention T. and F. in my list. :)  I think I've expressed a small distaste for T. in part because of the issues with defining it that we've discussed, but primarily because is very rarely used in mathematical literature beyond prop calc.  For example, _V is almost always defined as {x|x=x}; I've never seen {x|T} in set theory literature, and I like to be faithful to literature whenever possible.  For us, T. primarily serves a technical purpose inside of proofs as the heavy use of ~ trud shows, but I don't think it is used in any mainstream set.mm theorem beyond prop calc.

NAND was originally added specifically to study Nicod's single axiom for prop calc.  I don't know if NOR has been studied similarly.  My preference is not to add it, but if people feel strongly I guess I would accept it.

Norm

[Jim Kingdon]

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.

[Norman Megill]

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

[Norman Megill]

Posted per request of FL.

-------- Forwarded Message --------
Subject: Operators
Date: Sat, 25 Apr 2020 21:21:07 +0200 (CEST)
From: fl
To: Megill Norman

Let's agree: of course the opinion that we should confine ourselvesto the 5 classical operators for the formulation of the theorems. The study of the 11 other ones should be limited to one particular section: for example to prove that all of them can be expressed with NANDs etc.

-------- Forwarded Message --------
Subject: Parentheses
Date: Sat, 25 Apr 2020 21:33:38 +0200 (CEST)
From: fl
To: Megill Norman

Hi Norm,

Can you post this and also my my former mail.

I also wonder why not writing "( Word s ) " because the absence of parentheses can lead to expressions difficult to read. Suppose for instance that t* is also a predicate and not a function, we might have expressions like: Word t* S = t* Word S (it's silly. It's just to have an example of syntactical giberish).

--
FFL

[Benoit]

I agree with Norm that theorems of the form ?? <-> -. ?? should stay this way and not use XOR, which I've never seen used outside of propositional calculus.

Benoît

[Jim Kingdon]

> 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.

[Mario Carneiro]

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).

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/006246BC-0834-488B-97E2-5AD7F619A7DF%40panix.com.

[Alexander van der Vekens]

About 0 or 1 as first (or zeroth ;-) ?) index of words (see remarks of FL and Norm below):

Although there are good reasons to index the symbols of a word W by 1 .. length(W), there are also good reasons to start with 0. See, for example, Wikipedia https://en.wikipedia.org/wiki/Zero-based_numbering , especially the note of Edsger W. Dijkstra Why numbering should start at zero (https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD831.html) - Dijkstra would like our definition ( M ..^ N )...

Also the argument that using the modulo function is a good one - I used this for the proof of the friendship theorem, see, for example, ~cshwidx0mod. In the context of graph theory, it is useful to index the vertices in a walk, trail, path etc. of length n by 0 ... n and the edges by 0 ..^ n . Therefore, starting words with index 0 simplifies the definition of "walks as words" (see ~ df-wwlk), which I also used for the proof of the friendship theorem.

Since we are using 0 as first index already for several years, and there is a huge amount of theorems based on this definition (as already mentioned by Norm), I propose not to change the definition df-word. If there is a very good reason for a change in the future (which would justify the amount of work required to modify all existing related theorems), we can discuss this topic again.

On Saturday, April 25, 2020 at 7:29:25 PM UTC+2, Norman Megill wrote:

From FL:

...

I would also appreciate if the first index of a word is 1not 0. The C language has arrays that begins et 0 and its a pain un the neck because you always have to deal with n - 1 expressions.

From Norm:

...

[Benoit]

Like Alexander, I agree that word indices start at 0... like natural numbers ;-)

[Mario Carneiro]

FWIW I agree with Benoit and Alexander (and Dijkstra) on both counts. :)

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/95e2049c-c07c-40d7-b0e3-79061ef5327c%40googlegroups.com.

[David A. Wheeler]

The comments on the concatentation symbol, in ASCII and in presentation,
were all over the place. The symbol choice is not a deal-breaker for people :-).
The (Unicode) presentation options came down to ++ or frown,
while the ASCII representations came down to ++, '^', or concat.

I think the symbol and presentation of ++ was somewhat preferred
by more people, and the people who preferred frown would
be fine with ++. My attempt to (overly) simplify the preferences:
++: FL, Mario (doesn't want ASCII frown), David A. Wheeler (doesn't want ASCII frown)
++ _or_ "concat" as ASCII rep: Benoit [I think Benoit only focused on the ASCII form?]
Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not "concat");
Alexander also mentioned a compromise of "++" in ASCII but frown in presentation
frown in presentation: Norman Megill (but no issue changing to ++)

It was complicated to simplify the preferences; text snippets below.
My apologies in advance if I didn't accurately represent a current position or
missed somebody, please reply to correct!

I'll create a pull request to switch ASCII symbol "concat" to "++",
with presentation "++" (not the fancy Unicode symbol) per Norm's preference.
Then Norm can decide if he wants to accept it.

--- David A. Wheeler

=======================

Norman Megill:

I have no issue with changing "concat" to "++". As for the Unicode
symbol, I would lean towards just the simple "++" (two characters) rather
than "⧺" (which looks weird to me, almost suggesting "not parallel" rather
than 2 plus signs) but I'll go along with whatever people want.
Frown is also acceptable to me (maybe even my personal first choice, given
that it may be more common outside of computer science literature), maybe
with .^. or ^^ or '` (upside down df-cnv) as the ASCII token. But if more
people prefer ++ that is fine.

...

I'll also mention that Tarski used a frown symbol for concatenation in his
1965 paper. His notation is reproduced on p. 190 of the Metamath book,
using the LaTeX symbol "\frown".

Benoit:

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).

Alexander:

David A. Wheeler:

I have a minor preference for ++, but it's not a big deal to me.

In particular, I'd prefer "++" as the ASCII representation, with a Unicode display

of U+29FA and \doubleplus in LaTeX (package unicode-math).

This is somewhat common in Computer Science; Haskell uses "++"
for concatenation, and many other programming languages use "+" for concatenation
(but they can use types to figure out what overloaded operation was meant).
I think ++ would make the ASCII display a little simpler, and many people think of
"add" and "concatenate" as related... so having intentionally similar symbols
has some mild advantages.
Frown looks a little like intersection, even though there's no relationship,
and that could be considered a negative for it.
That said, frown has significant use, it's not terribly ambiguous,
and it just works, so I'm not unhappy with it.

... I think frown and doubleplus are the contenders.
(I don't like "no symbol", usually we try to make things obvious.)

Mario:

I like the idea of using ++ for concatenation, particularly in ascii
notation, since I don't want to try to reproduce a frown symbol in ascii. I
think the most common symbol for this is adjacency though.

FL: (Fri, 24 April 2020 - kicked this off)
I suggest that ++ replace concat. ...

[David A. Wheeler]

I'm going to pile on here. LIke Mario, Benoit, Alexander, and Dijkstra,
we should leave Word indexing as starting from 0.

It'd be a big change, with a lot of work, for no big benefit.
I haven't done a serious literature search, but I expect that the literature
will be inconsistent (just like it's inconsistent with the natural numbers).
If anything, I think there's been an increasing move towards 0-start
over 1-start over the last 100 years. Modulo is more inconvenient for 1-starting, too.

Let's leave Word as 0-starting (unchanged).

--- David A. Wheeler

[Norman Megill]

Posted per FL's request

Norm

-------- Forwarded Message --------
Subject: Dijkstra's argument
Date: Sun, 26 Apr 2020 17:31:09 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

can you post this.

Dijkstra's argument doesn't seem to apply to our problem. He is dealing with finding a good convention to speak of a sequence of natural numbers using <= or <. It is not at all our problem. We don't use order relations to speak of  a word.  He   also says  he prefers 0 because when you use the convention 0 <= x < N the bound  is N not  N +1. Once again it is not our problem: we don't use order relations. Our unique problem is what is better when we concatenate two words. And do we prefer our proofs are cluttered with expressions N - 1 or with the simpler N?

--
FL

[Mario Carneiro]

On Sun, Apr 26, 2020 at 17:31:09 +0200 (CEST) fl wrote:

Dijkstra's argument doesn't seem to apply to our problem. He is dealing with finding a good convention to speak of a sequence of natural numbers using <= or <. It is not at all our problem. We don't use order relations to speak of  a word.  He   also says  he prefers 0 because when you use the convention 0 <= x < N the bound  is N not  N +1. Once again it is not our problem: we don't use order relations. Our unique problem is what is better when we concatenate two words. And do we prefer our proofs are cluttered with expressions N - 1 or with the simpler N?

This is an interesting choice of argument because these seem to be exactly the places where the present state of affairs is strongest. As for 0 <= x < N, of course we use order relations, we don't write it that way but rather x e. ( 0 ..^ N ) and in that form it appears all over the place in the theory of words and otherwise. I agree the notation ..^ is a bit opaque; I prefer the notation used in Rust, where 0..n is our ( 0 ..^ n ) and 0..=n is our ( 0 ... n ). It makes it more obvious which one is the preferred notation, and it works great for for loops since you almost always want a simple for loop to range over 0 <= x < N.

As for concatenation, half open words have the beautiful identity ( A ..^ C ) = ( ( A ..^ B ) u. ( B ..^ C ) ), with no off by one errors. This alone makes them worthwhile to me. So if your worry is being "cluttered with expressions N - 1" then you should note that there is no such clutter in these expressions.

[Mario Carneiro]

Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not "concat");

By the way, I would like to reserve the notation '^' for the number 97, in preparation for possible formalization of ASCII. (In MM0 I'm using _char but 'char' is less likely to have overlapping usage.)

Mario

[heiph...@wilsonb.com]

Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'. Perhaps you mean't 94, which corresponds to the caret (i.e. '^')?

[Mario Carneiro]

Heh, beat me by 5 seconds. Indeed, I meant 94.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/39ZJ65EFIY1FP.3BA49F3SWBU0D%40wilsonb.com.

[Thierry Arnoux]

Hi all,

I've been aligning also the "Structured Typesetting" pages with the ++ notation for concatenation and ∆ (Uppercase Greek Delta) for symmetrical difference.

I also had to migrate the server on which those pages are hosted, the pages are currently being regenerated, thanks for your patience if the pages you are looking for are not available!

BR,
_
Thierry

[Mario Carneiro]

I think there is a unicode symbol for symmetric difference that is a white upward pointing triangle (U+25B3 △), not an upper case Delta (which looks a bit different due to weight changes along the glyph).

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/90500229-f562-475f-de53-ef2f2221c80b%40gmx.net.

[David A. Wheeler]

I propose that we move symmetric difference into the main body
of set.mm. It's a well-known-enough operation, and technically
we now have two mathboxes that use it :-). It's not large.
The move should be easy; just move everything with the
symbol /_\ somewhere, say "Define basic set operations and relations".

I should note that while inclusive-or is more common *today* in math,
historically exclusive-or (which is related to /_\ ) was often common.
Exclusive-or was the basis of Stoic logic, not inclusive-or, and Stoic logic
is the ancestor of propositional logic.

Mario:
> By the way, I would like to reserve the notation '^' for the number [94].

> in preparation for possible formalization of ASCII. (In MM0 I'm using _char
> but 'char' is less likely to have overlapping usage.)

I think formalization of ASCII is a cool idea, and I agree that
'^' (and so on) would be *MUCH* better notation than _^ (and so on).
If nothing else, the '...' notation is *widely* used to represent a single character,
and we should prefer common notations when we can.

I recommend that if you want to reserve that use - and I think you should -
then you should reserve it by adding those constants to your set.mm mathbox.
That way it will be immediately obvious to anyone else who sees set.mm
in the future. Nobody can remember everything, and if you do that, anyone else
who tries to use the term for another purpose will get an immediate error message.

--- David A. Wheeler

[Mario Carneiro]

On Sun, Apr 26, 2020 at 9:16 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

I think formalization of ASCII is a cool idea, and I agree that
'^' (and so on) would be *MUCH* better notation than _^ (and so on).
If nothing else, the '...' notation is *widely* used to represent a single character,
and we should prefer common notations when we can.

I know, and this is a bigger issue for set.mm than in the mm0 databases because these are smaller and more purpose driven. One reason I went with _c notations for characters is because it is easier to read

_h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d

than

'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd'

at least in monospace. But again, this is a luxury of not having a hundred competing notations from everything else in maths. For set.mm, the _c notations aren't really an option.

I recommend that if you want to reserve that use - and I think you should -
then you should reserve it by adding those constants to your set.mm mathbox.

I'd rather not, as ASCII is rather large and I don't like declaring a huge number of definitions in advance of use. Even in MM0 I've only declared about 40 or so characters from ASCII, only the ones I need in order to say what I need to. If I declare everything in advance then it's not clear where to stop, and heaven help us if we want anything from unicode.

Mario

[Thierry Arnoux]

You’re right! Actually, the code I used is x2206, which is listed as “Symmetrical Difference”, so I believe it shall be the correct one.

https://codepoints.net/U+2206

This is a different code from Uppercase Delta (code x394), I wanted to describe the shape - thanks for correcting me!

We can still use the x25B3 code (triangle) for geometry! ;-)

BR,

_

Thierry

Le 27 avr. 2020 à 11:44, Mario Carneiro <di....@gmail.com> a écrit :



[Mario Carneiro]

I'm not so sure about that. It looks like the primary meaning of that codepoint is "increment operator", used for small discrete changes, which usually is an actual Delta (and read as such aloud). Visually, it also shows the same typographic weight changes as is common with Delta that are absent in the white triangle symbol.

As for using the triangle symbol for geometry, well let's just say that's a conversation for another day.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/08094638-8C7B-47D9-814C-4E621E5C5B94%40gmx.net.

[heiph...@wilsonb.com]

FWIW, this Wikipedia list corresponds TeX's \triangle with U+2206:
https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject

> > <https://groups.google.com/d/msgid/metamath/08094638-8C7B-47D9-814C-4E621E5C5B94%40gmx.net?utm_medium=email&utm_source=footer>
> > .
> >

[Benoit]

I proposed the symbol for symmetric difference in https://github.com/metamath/set.mm/pull/1613#issuecomment-619592865 , namely U+25B3, after a quick google search for "unicode triangle". On the html pages, it looks a bit too large (ideally, it should be the same size as for \cap and \cup, especially the lower horizontal line).  But I cannot find the exact unicode for $\triangle$ ((edit: U+25B5 is definitely too small)).  The wikipedia page just cited is wrong: the symbol used in the first column corresponds to the LaTeX \triangle, but the columns "HTML" and "Unicode" correspond to other symbols.

(By the way: since the symmetric difference is commutative, it's nice to have a left-right symmetric symbol, so \Delta is not good.)

Benoît

On Monday, April 27, 2020 at 8:15:05 AM UTC+2, heiph...@wilsonb.com wrote:

FWIW, this Wikipedia list corresponds TeX's \triangle with U+2206:
https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject
Mario Carneiro <di....@gmail.com> wrote:
> I'm not so sure about that. It looks like the primary meaning of that
> codepoint is "increment operator", used for small discrete changes, which
> usually is an actual Delta (and read as such aloud). Visually, it also
> shows the same typographic weight changes as is common with Delta that are
> absent in the white triangle symbol.
>
> As for using the triangle symbol for geometry, well let's just say that's a
> conversation for another day.
>
>

> On Sun, Apr 26, 2020 at 10:12 PM Thierry Arnoux <thierr...@gmx.net>

> wrote:
>
> > You’re right! Actually, the code I used is x2206, which is listed as
> > “Symmetrical Difference”, so I believe it shall be the correct one.
> > https://codepoints.net/U+2206
> >
> > This is a different code from Uppercase Delta (code x394), I wanted to
> > describe the shape - thanks for correcting me!
> >
> > We can still use the x25B3 code (triangle) for geometry! ;-)
> > BR,
> > _
> > Thierry

> > file:///home/benoit/T%C3%A9l%C3%A9chargements/test.html

> >
> > Le 27 avr. 2020 à 11:44, Mario Carneiro <di....@gmail.com> a écrit :
> >
> > 
> > I think there is a unicode symbol for symmetric difference that is a white
> > upward pointing triangle (U+25B3 △), not an upper case Delta (which looks a
> > bit different due to weight changes along the glyph).
> >
> > --
> > 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 meta...@googlegroups.com.

[Thierry Arnoux]

See also this page:

https://www.unicode.org/charts/nameslist/n_2200.html

I agree we shall exclude the uppercase Delta, so we are left with x2206 and x25B3 as alternatives.

[heiph...@wilsonb.com]

Well, U+2206 (INCREMENT) is the only correctly oriented triangle I see in the
Mathematical Operators block (https://codepoints.net/mathematical_operators).
The U+25B3 (WHITE UP-POINTING TRIANGE) is part of the Geometric Shapes block
(https://codepoints.net/geometric_shapes).

Looking at the individual pages for each character:

- https://codepoints.net/U+2206, and
- https://codepoints.net/U+25B3,

codepoints.net does claim that U+2206 is used for set symmetric difference.
That said, U+25B3 certainly looks a lot more symmetric in the typeface it's
rendering as on my machine.

Each page also gives a nice set of "confusables." Each of the above two
characters lists the other in that section. How about U+1F702 (ALCHEMAL
SYMBOL FOR FIRE) though! ;p

Benoit <benoit...@gmail.com> wrote:
> I proposed the symbol for symmetric difference in
> https://github.com/metamath/set.mm/pull/1613#issuecomment-619592865 ,
> namely U+25B3, after a quick google search for "unicode triangle". On the
> html pages, it looks a bit too large (ideally, it should be the same size
> as for \cap and \cup, especially the lower horizontal line). But I cannot

> find the exact unicode for $\triangle$. The wikipedia page just cited is

> wrong: the symbol used in the first column corresponds to the LaTeX
> \triangle, but the columns "HTML" and "Unicode" correspond to other symbols.
>
> (By the way: since the symmetric difference is commutative, it's nice to
> have a left-right symmetric symbol, so \Delta is not good.)
>
> Benoît
>
>
> On Monday, April 27, 2020 at 8:15:05 AM UTC+2, heiph...@wilsonb.com wrote:
> >
> > FWIW, this Wikipedia list corresponds TeX's \triangle with U+2206:
> > https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject

> > Mario Carneiro <di....@gmail.com <javascript:>> wrote:
> > > I'm not so sure about that. It looks like the primary meaning of that
> > > codepoint is "increment operator", used for small discrete changes,
> > which
> > > usually is an actual Delta (and read as such aloud). Visually, it also
> > > shows the same typographic weight changes as is common with Delta that
> > are
> > > absent in the white triangle symbol.
> > >
> > > As for using the triangle symbol for geometry, well let's just say
> > that's a
> > > conversation for another day.
> > >
> > >
> > > On Sun, Apr 26, 2020 at 10:12 PM Thierry Arnoux <thierr...@gmx.net

> > <javascript:>>

> > > wrote:
> > >
> > > > You’re right! Actually, the code I used is x2206, which is listed as
> > > > “Symmetrical Difference”, so I believe it shall be the correct one.
> > > > https://codepoints.net/U+2206
> > > >
> > > > This is a different code from Uppercase Delta (code x394), I wanted to
> > > > describe the shape - thanks for correcting me!
> > > >
> > > > We can still use the x25B3 code (triangle) for geometry! ;-)
> > > > BR,
> > > > _
> > > > Thierry
> > > > file:///home/benoit/T%C3%A9l%C3%A9chargements/test.html
> > > >
> > > > Le 27 avr. 2020 à 11:44, Mario Carneiro <di....@gmail.com

> > <javascript:>> a écrit :

> > > >
> > > > 
> > > > I think there is a unicode symbol for symmetric difference that is a
> > white
> > > > upward pointing triangle (U+25B3 △), not an upper case Delta (which
> > looks a
> > > > bit different due to weight changes along the glyph).
> > > >
> > > > --
> > > > 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 meta...@googlegroups.com <javascript:>.

[Norman Megill]

On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
...

I know, and this is a bigger issue for set.mm than in the mm0 databases because these are smaller and more purpose driven. One reason I went with _c notations for characters is because it is easier to read

_h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d

than

'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd'

Maybe I missed something in this thread, but what is the purpose of formalizing ASCII?  Is this something that eventually might be added to set.mm?.

Our informal convention has been to prefix non-italic letters with underscore, like _i, so _<letter> will clash with a few that already exist.  How about a single quote prefix, 'a 'b 'c ... like in Lisp 'foo to abbreviate (quote foo)?  That would not clash with anything in set.mm except ''' in AV's mathbox (for alternate function value) which could be changed.

    'h : 'e : 'l : 'l : 'o : 'sp : 'w : 'o : 'r : 'l : 'd

Norm

[Norman Megill]

Posted per FL's request.

-------- Forwarded Message --------
Subject: Scheffer stroke
Date: Mon, 27 Apr 2020 19:21:36 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

can you post this:

In the commentary it is saïd that it is Russel and Whitehead who discovered that NAND can be used as the one connector necessary to define the other ones. According to Wikipedia (article "Scheffer stroke") it is Scheffer who discovered this fact in 1913. Maybe the commentary should be fixed. Whitehead and Russel made a reference to this discovery in the second edition of Principia Mathematica in the 20s.

--
FL

[Benoit]

Then U+25B3 (the current symbol) it is, for symmetry reasons (and to stay away from alchemistry).

Benoît

On Monday, April 27, 2020 at 12:20:56 PM UTC+2, heiph...@wilsonb.com wrote:

Well, U+2206 (INCREMENT) is the only correctly oriented triangle I see in the
Mathematical Operators block (https://codepoints.net/mathematical_operators).
The U+25B3 (WHITE UP-POINTING TRIANGE) is part of the Geometric Shapes block
(https://codepoints.net/geometric_shapes).

Looking at the individual pages for each character:

- https://codepoints.net/U+2206, and
- https://codepoints.net/U+25B3,

codepoints.net does claim that U+2206 is used for set symmetric difference.
That said, U+25B3 certainly looks a lot more symmetric in the typeface it's
rendering as on my machine.

Each page also gives a nice set of "confusables." Each of the above two
characters lists the other in that section. How about U+1F702 (ALCHEMAL
SYMBOL FOR FIRE) though! ;p

[Mario Carneiro]

On Mon, Apr 27, 2020 at 7:35 AM Norman Megill <n...@alum.mit.edu> wrote:

On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
...

I know, and this is a bigger issue for set.mm than in the mm0 databases because these are smaller and more purpose driven. One reason I went with _c notations for characters is because it is easier to read

_h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d

than

'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd'

Maybe I missed something in this thread, but what is the purpose of formalizing ASCII?  Is this something that eventually might be added to set.mm?.

I didn't explain this, but I am already using a formalization of ASCII in MM0, for example https://github.com/digama0/mm0/blob/master/examples/mm0.mm0#L405-L459 . As you can see there, it is being used in order to define the input language of MM0 so that I can make a claim about an MM0 verifier. While I have no immediate plans to move this to set.mm, this is a possibility, and it also shows an example of a mathematically reasonable use of ASCII formalization, which may come up in set.mm in another form (e.g. metamath in metamath).

Our informal convention has been to prefix non-italic letters with underscore, like _i, so _<letter> will clash with a few that already exist.  How about a single quote prefix, 'a 'b 'c ... like in Lisp 'foo to abbreviate (quote foo)?  That would not clash with anything in set.mm except ''' in AV's mathbox (for alternate function value) which could be changed.

    'h : 'e : 'l : 'l : 'o : 'sp : 'w : 'o : 'r : 'l : 'd

This also works for me. I don't think it is essential to commit to a notation right now since I'm not actually adding these characters to set.mm, but I wanted to make sure that others keep this use in mind.

Mario

[David A. Wheeler]

On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
> >> I know, and this is a bigger issue for set.mm than in the mm0 databases
> >> because these are smaller and more purpose driven. One reason I went with
> >> _c notations for characters is because it is easier to read
> >> _h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d
> >> than
> >> 'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd'

On Mon, Apr 27, 2020 at 7:35 AM Norman Megill <n...@alum.mit.edu> wrote:
> > Maybe I missed something in this thread, but what is the purpose of
> > formalizing ASCII? Is this something that eventually might be added to
> > set.mm?.

On Mon, 27 Apr 2020 18:10:05 -0700, Mario Carneiro <di....@gmail.com> wrote:
> While I have no
> immediate plans to move this to set.mm, this is a possibility, and it also
> shows an example of a mathematically reasonable use of ASCII formalization,
> which may come up in set.mm in another form (e.g. metamath in metamath).

All by itself that's a potentially interesting use (metamath in metamath).

Norman Megill:

> > Our informal convention has been to prefix non-italic letters with
> > underscore, like _i, so _<letter> will clash with a few that already
> > exist. How about a single quote prefix, 'a 'b 'c ... like in Lisp 'foo to
> > abbreviate (quote foo)?
> > That would not clash with anything in set.mm
> > except ''' in AV's mathbox (for alternate function value) which could be
> > changed.

I like that convention. Especially since I know Lisp :-).

Mario:

> This also works for me. I don't think it is essential to commit to a
> notation right now since I'm not actually adding these characters to set.mm,
> but I wanted to make sure that others keep this use in mind.

It may not be *essential*, but I think it would be wise to "reserve" these
symbols for future use. Usually we add 1-2 symbols at a time, but if we ever
add a representation of ASCII, we'd want to add a large set with exactly the
same rule (whatever that is). If we reserve them now & don't use them, no big deal.
If we don't reserve them, we might we have to do a lot of renaming and other nonsense
to have a large set of symbols with a consistent convention.

I'll try to make a pull request to define 'LETTER for a set, so that people will be
automatically warned if they try to define an operation for some other purpose.
That will "reserve" the pattern for potential use later.

--- David A. Wheeler

[Jim Kingdon]

> it is being used in order to define the input language of MM0 so that I can make a claim about an MM0 verifier

Ah, and here I had let my hopes get up that it was for formalizing Gödel's Incompleteness Theorem (which is in the Metamath 100, after all).

[Mario Carneiro]

Hey, I didn't say that was *all* it's for. It's not on the top of my list of priorities, but I believe that the project will be in a good position to formalize Godel's incompleteness theorem once the main goal is finished. Already we have enough to formalize inductively defined structures like expression trees and Godel numbering; if I recall the proof correctly there isn't that much more to do to diagonalize it.

Mario