Logic Symbols
Forty-six logic characters with the codepoint and official Unicode name each one carries, including the character Unicode provides for such that. The notes cover the turnstiles, the two tacks whose names read backwards, and the arrow that is not the same kind of character as its partners.
Tap any tile to copy it. Nothing is sent anywhere — the copy happens in your browser.
The characters that carry ordinary logic
∀ U+2200 FOR ALL and ∃ U+2203 THERE EXISTS are the quantifiers. ¬ U+00AC NOT SIGN negates. ∧ U+2227 LOGICAL AND and ∨ U+2228 LOGICAL OR join. ⇒ U+21D2 RIGHTWARDS DOUBLE ARROW and ⇔ U+21D4 LEFT RIGHT DOUBLE ARROW carry implication and equivalence, and ∴ U+2234 THEREFORE and ∵ U+2235 BECAUSE mark a conclusion and a reason. That is most of working logic in nine characters; the other thirty-seven are turnstiles, tacks and variants of the connectives.
The character for “such that”
∍ U+220D SMALL CONTAINS AS MEMBER is the character Unicode provides for it — the small form of ∋ U+220B CONTAINS AS MEMBER, which is U+2208 ELEMENT OF written the other way round. It is not the only way: a colon and a vertical bar both do the job, and both are ASCII, so they survive a form field or a filename that ∍ will not. Use ∍ where the text is read by a person and the ASCII marks where it is read by a parser.
One bar and two bars are not the same claim
⊢ U+22A2 RIGHT TACK is the turnstile: the formula on the right can be derived from what is on the left, by the rules of some proof system. ⊧ U+22A7 MODELS says something different — that the formula is true in every structure satisfying the left side. Syntax against meaning, and swapping one for the other changes the claim. ⊦ U+22A6 ASSERTION is a second single-bar form; ⊣ U+22A3 LEFT TACK is its mirror. The double turnstile usually typeset for entailment, U+22A8 TRUE, is not in this set.
⊤ and ⊥ are named the opposite way round from how they are read
⊤ U+22A4 is officially DOWN TACK and is the constant for truth, spoken as “top”. ⊥ U+22A5 is UP TACK and is the constant for falsity, spoken as “bottom”. The names describe which way the stroke points, not what the character means, so a database search for “top” or “bottom” finds neither. Look them up by tack.
The three double arrows are not one family
⇒ and ⇔ are general category Sm, maths symbols, with East Asian width Ambiguous. ⇐ U+21D0 LEFTWARDS DOUBLE ARROW is category So and width Neutral. They are drawn as a matched set and do not behave as one: a filter that keeps only Sm drops the leftwards arrow and keeps its partners, and in a terminal rendering ambiguous characters wide the leftwards arrow is one cell where the others are two. In a monospace proof column, that is what pulls it out of alignment.
∧ and ⋀ do different jobs
∧ joins two formulae. ⋀ U+22C0 N-ARY LOGICAL AND is the big operator that takes an index range underneath it, the way a summation sign does, standing for a conjunction over a whole family. ∨ and ⋁ split the same way.
Width and encoding
¬ is width Narrow and sits below U+0100, so latin-1 and cp1252 carry it as a single byte — it is the only character in this set that survives a latin-1 channel. ∀, ∃, ∧, ∨, ∴, ∵, ∋, ⊥, ⇒ and ⇔ are width Ambiguous; apart from ¬, everything else is Neutral. A field that strips non-ASCII removes every one of them and leaves the surrounding words intact — the version of this failure hardest to notice.
The wing index is the maths and science symbols list. The single-stroke arrows are on arrow symbols, and the membership and inclusion relations these formulae quantify over are on set theory symbols.