Re: symbols/codepoints for necessity and possibility in modal logic

> What is wrong with using DIAMOND OPERATOR?
"wrong" is strong wording and goes beyond what I suggested or implied,
but it's not clear to a user of Unicode that it's the right fit either.
There are a couple of indicators factoring in:

  * The charts mention modal logic in conjunction with ◻ (U+25FB) and ⟠
    (U+27E0) but not with ⋄ (U+22C4).
  * The glyph in the code charts is tiny (and that of Cambria Math is
    tiny as well). Typographically you see various things (a lozenge,
    fallback to letter-M) in esp older books, but it feels like it's
    meant to be an orthogonal diamond of perhaps slightly less area than
    the box but descending a little above and below the box, which is
    somewhat taller than x-height. The book by {Blackburn, de Rijke,
    Venema} has glyphs that look right. This is more than a guess: it
    makes sense if they have similar visual weight, as they are –
    literally – defined to be duals of one another; but whether you can
    make them geometrically congruent symbols of equal area I haven't
    tested (this might have the diamond ascend too far).
  * The vague notion of "operator" (a word with different meanings in
    math, from /logical relation/ to /[non-logical/non-relational]
    mapping of type A×A→A or perhaps A×A→B/ to /(linear) map (between
    say vector spaces) in linear algebra/) in this context (in the code
    charts) seems to refer to something like my middle meaning, which is
    likely to use a smaller symbol around x-height in placement and
    dimensions.
  * The glyph of ⬦ (U+2B26) seems to have a more appropriate name, but
    in the charts I like ◇ U+25C7. The differently sized square-like
    symbols are hard to semantically tell apart in/from the charts anyway.
  * These symbols are the first two visually distinct ones you define in
    modal logic, so they're well-known and standardized in meaning for
    anyone who had had contact with the field. It's surprising they're
    not explicitly named in the charts. (There's stuff like the outdated
    horseshoe for logical implication popping up in the relevant books,
    but that is a leftover or outdated logic notation in general.) So
    for box and diamond it's quite reasonable to be expecting a standard
    math font to provide them just right out of the box; for whatever
    commonly used box-like symbols in math there are, one would assume
    that there are corresponding codepoints; otherwise you'd have to
    choose a different font.

Stephan
Received on Fri Jul 19 2013 - 02:47:15 CDT