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.