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

There is the white square with leftwards tick (⟤, U+27E4), which
supposedly means “was always”, but no “regular” (non-concave-sided)
white diamond with leftwards tick. Hence, I suspect that U+27E1 (⟡) is
simply used as a temporal equivalent to U+25C7 (though I know that
usually just U+25C7 is used) and expect U+27E2 (⟢) to mean “was at
some time” rather than “was never”.

Julian Bradfield via Unicode <[email protected]>:
>
> On 2024-09-16, Ivan Panchenko via Unicode <[email protected]> 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'!
>