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'! >
