Does U+27E1 really mean “never” rather than “sometimes”?

[Julian Bradfield]

On 2024-09-16, Ivan Panchenko via Unicode <unicode at corp.unicode.org> wrote:
> The white concave-sided diamond (⟡) has the informative alias “never
> (modal operator)”. I would have expected it to mean the opposite
> because U+25C7 (◇, white diamond) is used for possibility rather than
> impossibility. Two sources that support my view:

I can't say, as a sometimes practising modal logician, that I've ever
seen this symbol as a distinct grapheme. In particular

> https://books.google.com/books?id=41VYDwAAQBAJ&pg=PA211

This is not semantically ⟡ distinct from some other diamond, it's just
a diamond that has been designed slightly concave; or if it is
actually a distinct character in the font, it's an authorial choice
(or error), as it's clear from the text that the author is intending
the standard modal diamond, which is used for `possibly' in modal
logic and `sometime' in temporal logic.

> https://www.mdpi.com/2079-9292/8/10/1163

This paper is the area I used to work in.
Here one can see that the diamond is indeed U+27E1, but nonetheless the
author is using completely standard notation for LTL, and is, either
through the random facilities of their authoring software or
deliberate aesthetic choice, using a concave diamond rather than a
straight diamond. 

You should be looking for an author who uses straight and concave
diamonds contrastively. I imagine that somebody has, though personally
I would consider it a perverse notation to make ⟡ mean `never'!