Mathematical Logic Symbols

This page contains 28 mathematical logic symbols, covering basic propositional connectives (negation, conjunction, disjunction, implication, equivalence), exclusive or, equivalence, NAND, NOR, universal quantifiers, existential quantifiers, unique quantifiers in predicate logic, logical consequence, assertions, truth constants, and QED symbols in proof theory. These symbols play a central role in mathematical foundations, theoretical computer science, artificial intelligence, formal verification, and mathematical logic research. Below is a systematic introduction to the mathematical meaning, technical parameters, LaTeX typesetting, and usage notes for each symbol.

🔗 Basic Propositional Connectives

¬ is called the "Negation" symbol. It represents logical NOT, used to negate propositions. Its Unicode is U+00AC, the LaTeX command is \neg or \lnot, and the HTML entity is ¬.

∧ is called the "Conjunction" symbol. It represents logical AND, meaning "and". Its Unicode is U+2227, the LaTeX command is \land or \wedge, and the HTML entity is ∧.

∨ is called the "Disjunction" symbol. It represents logical OR. Its Unicode is U+2228, the LaTeX command is \lor or \vee, and the HTML entity is ∨.

⇒ is called the "Implication" symbol. It means "if...then...". Its Unicode is U+21D2, the LaTeX command is \Rightarrow, and the HTML entity is ⇒.

⇔ is called the "Equivalence" symbol. It means "if and only if". Its Unicode is U+21D4, the LaTeX command is \Leftrightarrow, and the HTML entity is ⇔. Note the distinction from biconditional assignment; \iff is recommended for better spacing in LaTeX.

✨ Extended Logical Operations

⊕ is called the "XOR" symbol. It represents exclusive or, commonly used in cryptography and circuit design. Its Unicode is U+2295, the LaTeX command is \oplus, and the HTML entity is ⊕.

⊻ is an alternative "XOR" symbol. Its Unicode is U+22BB, the LaTeX command is \veebar, and the HTML entity is ⊻.

⊗ is called the "XNOR" symbol. It represents the negation of XOR (equivalence). Its Unicode is U+2297, the LaTeX command is \otimes, and the HTML entity is ⊗.

⊼ is called the "NAND" symbol. It represents conjunction followed by negation. Its Unicode is U+22BC, the LaTeX command is \barwedge (or \nand with a package), and the HTML entity is ⊼.

⊽ is called the "NOR" symbol. It represents disjunction followed by negation. Its Unicode is U+22BD, the LaTeX command is custom (\nor), and the HTML entity is ⊽.

↔️ Implication Relations

⇐ is called the "Reverse Implication" symbol. It represents "only if". Its Unicode is U+21D0, the LaTeX command is \Leftarrow, and the HTML entity is ⇐.

⇏ is called the "Non-Implication" symbol. It represents failed implication. Its Unicode is U+21CF, the LaTeX command is \nRightarrow, and the HTML entity is ⇏.

⇍ is called the "Non-Reverse Implication" symbol. It represents reverse non-implication. Its Unicode is U+21CD, the LaTeX command is \nLeftarrow, and the HTML entity is ⇍.

∀ Quantifiers & Predicate Logic

∀ is called the "Universal Quantifier". It means "for all". Its Unicode is U+2200, the LaTeX command is \forall, and the HTML entity is ∀.

∃ is called the "Existential Quantifier". It means "there exists". Its Unicode is U+2203, the LaTeX command is \exists, and the HTML entity is ∃.

∄ is called the "Non-Existence Quantifier". It means "there does not exist". Its Unicode is U+2204, the LaTeX command is \nexists, and the HTML entity is ∄.

s.t. is the abbreviation for "such that", widely used in set notation. Its LaTeX command is \text{ s.t. }.

p.j. is a classical notation for "propositionis j", preserved as a historical logic symbol. Its LaTeX command is \text{p.j.}.

⊢ Proof Theory & Truth Constants

⊤ is called the "Tautology" symbol. It represents logical truth. Its Unicode is U+22A4, the LaTeX command is \top, and the HTML entity is ⊤.

⊥ is called the "Contradiction" symbol. It represents logical falsity. Its Unicode is U+22A5, the LaTeX command is \bot, and the HTML entity is ⊥.

⊢ is called the "Turnstile" symbol. It means "derives" or "proves", used in sequent calculus. Its Unicode is U+22A2, the LaTeX command is \vdash, and the HTML entity is ⊢.

⊣ is called the "Reverse Turnstile" symbol. It represents reverse derivation. Its Unicode is U+22A3, the LaTeX command is \dashv, and the HTML entity is ⊣.

⊨ is called the "Models" symbol. It represents logical validity or satisfaction. Its Unicode is U+22A8, the LaTeX command is \models, and the HTML entity is ⊧.

⊩ is called the "Forcing" symbol. It is used in forcing methods and Kripke semantics. Its Unicode is U+22A9, the LaTeX command is \Vdash, and the HTML entity is ⊩.

∴ Inference & QED Symbols

∴ is called the "Therefore" symbol. It represents logical conclusion, used in geometric proofs and logic. Its Unicode is U+2234, the LaTeX command is \therefore, and the HTML entity is ∴.

∵ is called the "Because" symbol. It represents premise. Its Unicode is U+2235, the LaTeX command is \because, and the HTML entity is ∵.

∎ is called the "QED" symbol. It marks the end of a proof. Its Unicode is U+220E, the LaTeX command is \qed or \blacksquare, and the HTML entity is ∎.

Q.E.D. is the Latin abbreviation for "quod erat demonstrandum", traditionally used at the end of proofs. Its LaTeX command is \text{Q.E.D.}.

📌 Usage & Typesetting Guidelines

When typesetting mathematical logic symbols: 1. Use \neg for negation (¬), not a tilde or hyphen in LaTeX. 2. \land is recommended over \wedge for conjunction (∧) for readability. 3. Distinguish implication (⇒, \Rightarrow) from function arrows (→, \to). 4. Quantifiers (∀, ∃) can be used inline with subscripts for restrictions. 5. \vdash (syntactic consequence) and \models (semantic consequence) are not interchangeable. 6. Use \oplus for XOR (⊕). 7. Use \square or \blacksquare for QED symbols. 8. Text abbreviations (s.t., p.j.) should be placed inside \text{} in formulas. Proper usage enhances the professionalism of logic papers and formal documents.

💡 Usage Tips

To copy Unicode, LaTeX commands, or HTML entities, click the corresponding symbol card above and select the desired item in the details panel. Each symbol can generate SVG source code or be downloaded as a 512×512 transparent PNG image for design and documentation. For logic papers and computer science reports, LaTeX commands are recommended for optimal typesetting, ensuring consistent spacing and fonts in complex derivations.