Logic symbols: meanings, LaTeX, Unicode and how to type them
Logic symbols and what they mean: ¬ not, ∧ and, ∨ or, → if … then, ↔ if and only if, and the quantifier and proof symbols ∀, ∃, ⊢, ⊨ and ∴. The table below gives each symbol’s LaTeX, Unicode and HTML code; further down are the spellings Tangibool’s tools accept and how to type each symbol.
| Symbol | Name | Read as | Meaning | LaTeX | Unicode | HTML | In Tangibool’s tools |
|---|---|---|---|---|---|---|---|
| ¬ | negation | not p | true when p is false | \neg, \lnot | U+00AC | ¬ | accepted, as are NOT, ! and p' |
| ∧ | conjunction | p and q | true when both are true | \land, \wedge | U+2227 | ∧ | accepted, as are AND, && and · |
| ∨ | disjunction | p or q | true when at least one is true | \lor, \vee | U+2228 | ∨ | accepted, as are OR, || and + |
| ⊕ | exclusive or | p xor q | true when exactly one of the two is true | \oplus | U+2295 | ⊕ | accepted, as is XOR |
| → | conditional (implication) | if p then q | false only when p is true and q is false | \rightarrow, \to | U+2192 | → | accepted, as is -> |
| ↔ | biconditional | p if and only if q | true when p and q have the same value | \leftrightarrow | U+2194 | ↔ | accepted, as is <-> |
| ⇒ | implies | p implies q | as →; often written between statements rather than inside a formula | \Rightarrow, \implies | U+21D2 | ⇒ | not accepted: type -> |
| ⊃ | horseshoe (older texts) | p implies q | as → | \supset | U+2283 | ⊃ | not accepted: type -> |
| ⇔ | equivalence | p is equivalent to q | as ↔; often written between statements | \Leftrightarrow, \iff | U+21D4 | ⇔ | not accepted: type <-> |
| ≡ | logical equivalence | p is equivalent to q | the same truth value on every row | \equiv | U+2261 | ≡ | not accepted: compare two formulas in the equivalence checker |
| ⊤ | top | true | always true | \top | U+22A4 | ⊤ | not accepted: type TRUE or 1 |
| ⊥ | bottom | false | always false; also marks a contradiction | \bot | U+22A5 | ⊥ | not accepted: type FALSE or 0 |
| ⊻ | exclusive or (variant) | p xor q | as ⊕ | \veebar | U+22BB | ⊻ | not accepted: type XOR or ⊕ |
| ⊼ | NAND | p nand q | true unless both are true | \barwedge | U+22BC | ⊼ | not accepted: type NAND(p, q) |
| ⊽ | NOR | p nor q | true when both are false | none in the base packages | U+22BD | ⊽ | not accepted: type NOR(p, q) |
| ∀ | universal quantifier | for all x | the statement holds for every x | \forall | U+2200 | ∀ | not used: the tools work with propositional logic |
| ∃ | existential quantifier | there exists an x | the statement holds for at least one x | \exists | U+2203 | ∃ | not used |
| ⊢ | turnstile | proves | the right side can be derived from the left by the rules of a proof system | \vdash | U+22A2 | ⊢ | not used |
| ⊨ | double turnstile | entails, models | the right side is true whenever the left side is | \models, \vDash | U+22A8 | ⊨ | not used; the argument validity checker answers this question for propositional logic |
| ∴ | therefore | therefore | marks a conclusion | \therefore | U+2234 | ∴ | not used |
| ∵ | because | because | marks a reason | \because | U+2235 | ∵ | not used |
| ∎ | end of proof | QED | the proof is complete | \blacksquare, or \qed in amsthm (an open box) | U+220E | ∎ | not used |
The four notations are interchangeable on input and selectable on output. NOT A, !A, ¬A and A' are one formula; A AND B, A && B, A ∧ B and A·B are one formula; A OR B, A || B, A ∨ B and A + B are one formula. Exclusive or is XOR or ⊕, implication -> or →, the biconditional <-> or ↔, and the constants TRUE, FALSE, 1 and 0. Operator words are case-insensitive, so a AnD b parses, but the names of inputs are not.
Three gates have only a function spelling, NAND(A, B), NOR(A, B) and XNOR(A, B), each with exactly two operands, and two indexed forms name a function by its rows: Σm(A, B; 1, 2) lists the minterms and ΠM(A, B; 0) the maxterms, with minterms(…) and maxterms(…) as plain-text spellings. Output definitions use :=, which is why a bare = inside a formula is rejected.
The rejected spellings are the ones that mean something else somewhere: = and == (comparison, not an operator here), != (which on Booleans is XOR), => and <=> (fat arrows that vary between tools), ~ (bitwise in C), &, | and ^ (bitwise in C, Java and JavaScript), * (arithmetic), the infix A NAND B, and two names side by side (A B), which some textbooks read as multiplication. In every case the parser names the problem and offers a repair, and the readings below are recorded from the parser itself at build time.
Accepted spellings
| Operator | Accepted spellings | Words | Programming | Mathematical | Algebra |
|---|---|---|---|---|---|
| not | NOT ! ¬ a' a′ | NOT a | !a | ¬a | a' |
| and | AND && ∧ · ⋅ | a AND b | a && b | a ∧ b | a·b |
| or | OR || ∨ + | a OR b | a || b | a ∨ b | a + b |
| xor | XOR ⊕ | a XOR b | a XOR b | a ⊕ b | a ⊕ b |
| implies | -> → | a -> b | a -> b | a → b | a → b |
| iff | <-> ↔ | a <-> b | a <-> b | a ↔ b | a ↔ b |
| nand | NAND(a, b) | NAND(a, b) | NAND(a, b) | NAND(a, b) | NAND(a, b) |
| nor | NOR(a, b) | NOR(a, b) | NOR(a, b) | NOR(a, b) | NOR(a, b) |
| xnor | XNOR(a, b) | XNOR(a, b) | XNOR(a, b) | XNOR(a, b) | XNOR(a, b) |
| minterms | Σm(a, b; 1, 3) ∑m(…) minterms(…) | Σm(a, b; 1, 3) | Σm(a, b; 1, 3) | Σm(a, b; 1, 3) | Σm(a, b; 1, 3) |
| maxterms | ΠM(a, b; 0) ∏M(…) maxterms(…) | ΠM(a, b; 0) | ΠM(a, b; 0) | ΠM(a, b; 0) | ΠM(a, b; 0) |
| constants | TRUE FALSE 1 0 | TRUE / FALSE | TRUE / FALSE | 1 / 0 | 1 / 0 |
Rejected spellings and their repairs
| You typed | Code | Why it is rejected | Repair offered |
|---|---|---|---|
| A = B | unsupported-operator | `=` is not an expression operator. Use `<->` when both sides must have the same value; compare whole formulas in the Compare workbench. Output definitions use `:=`. | Replace with <-> |
| A == B | unsupported-operator | `==` is not an expression operator. Use `<->` when both sides must have the same value, or the Compare workbench to compare two formulas. | Replace with <-> |
| A != B | unsupported-operator | `!=` is not an expression operator. Use `XOR` when the two sides must differ. | Replace with XOR |
| A => B | unsupported-operator | `=>` is not a supported operator. Use `->` for implication. | Replace with -> |
| A <=> B | unsupported-operator | `<=>` is not a supported operator. Use `<->` for a biconditional. | Replace with <-> |
| ~A | unsupported-operator | `~` is not a supported operator. Use `NOT`, `!`, or `¬` for negation. | Replace with NOT |
| A & B | unsupported-operator | A single `&` is not supported. Use `AND` or `&&`. | Replace with AND Replace with && |
| A | B | unsupported-operator | A single `|` is not supported. Use `OR` or `||`. | Replace with OR Replace with || |
| A ^ B | unsupported-operator | `^` is not supported (it is bitwise in many languages). Use `XOR` or `⊕`. | Replace with XOR |
| A * B | unsupported-operator | `*` is not supported. Use `AND`, `&&`, `∧`, or the algebra product `·`. | Replace with AND Replace with · |
| A NAND B | infix-function | NAND uses function notation, e.g. NAND(A, B). | Rewrite as NAND(A, B) |
| A B | missing-operator | Missing operator between `A` and `B`. Implicit multiplication is not supported — write the operator explicitly. | Insert AND Insert OR |
| not A == B | unsupported-operator | `==` is not an expression operator. Use `<->` when both sides must have the same value, or the Compare workbench to compare two formulas. | Replace with <-> |
Several symbols for one operator
Textbooks, programming languages and logic courses write the same operator in different ways. Negation is ¬p, ~p, !p, p′ or p with a bar over it. Conjunction is p ∧ q, p · q, pq, p & q or p && q. Disjunction is p ∨ q, p + q, p | q or p || q. Implication is p → q, p ⇒ q or p ⊃ q, and the biconditional is p ↔ q, p ⇔ q or p ≡ q. NAND is also written p ↑ q or p | q, the Sheffer stroke, and NOR p ↓ q, the Peirce arrow, so the vertical bar means OR in code and NAND in some logic books.
Tangibool’s tools read the operator words, the symbols ¬, ∧, ∨, ⊕, → and ↔, the programming forms and the algebra forms, and they refuse the spellings that mean different things in different places, such as ~, &, | and ^, with a message and a repair. The two tables above list both.
Quantifier and proof symbols
∀ and ∃ belong to predicate logic, which talks about every x or some x: ∀x P(x) says that every x has the property P, and ∃x P(x) that at least one does. Negation swaps them: ¬∀x P(x) means the same as ∃x ¬P(x), so “not all” means “at least one does not”.
⊢ and ⊨ make statements about formulas rather than combining them. Γ ⊢ φ says that φ can be derived from the premises Γ by the rules of a proof system; Γ ⊨ φ says that φ is true in every case where all of Γ is true. For propositional logic the two agree, and the argument validity checker answers the ⊨ question by checking every row.
∴ and ∵ mark the conclusion and the reason of a written argument, and ∎ or □ ends a proof. Tangibool’s tools work with propositional formulas, so none of these symbols is part of their input.
Set symbols
Discrete mathematics courses use set symbols beside the logic ones, and each mirrors a connective: x is in A ∪ B when x ∈ A or x ∈ B, and in A ∩ B when x ∈ A and x ∈ B. The common ones are ∈, element of (\in, ∈); ∉, not an element of (\notin, ∉); ⊆, subset (\subseteq, ⊆); ⊂, subset or, in some books, proper subset (\subset, ⊂); ∪, union (\cup, ∪); ∩, intersection (\cap, ∩); and ∅, the empty set (\emptyset, ∅).
How to type logic symbols
Microsoft Word. Insert › Symbol › More Symbols, then the Mathematical Operators subset. In Word for Windows you can also type the code and press Alt+X: 2227 then Alt+X gives ∧, and 00AC gives ¬. Inside an equation (Alt+= on Windows, or Insert › Equation), type \wedge, \vee, \neg, \rightarrow, \leftrightarrow, \forall or \exists followed by a space.
Google Docs. Insert › Special characters, then search by name, for example “logical and”. Inside an equation (Insert › Equation), LaTeX-style commands such as \rightarrow and \forall followed by a space insert the symbol.
macOS. Option+L types ¬ on the US and British keyboard layouts. For the others, open the Character Viewer with Control+Command+Space and search by name, or add the Unicode Hex Input keyboard and hold Option while typing the four-digit code.
Windows. Win+. opens the emoji panel, whose symbols tab includes maths symbols, and Character Map finds any character by name. Alt+0172 on the numeric keypad types ¬.
LaTeX. Use the commands in the table, in maths mode. \veebar, \barwedge, \vDash, \therefore, \because and \blacksquare need the amssymb package, \implies needs amsmath and \qed comes with amsthm; the rest work in plain LaTeX. The LaTeX page has the whole notation.
HTML. Use the named codes in the table, such as ∧, or the numeric form, such as ∧, which works for every symbol.
The common slip
Pasting a formula from a textbook or a program and trusting that it parsed as intended. AB + C' is accepted only as A·B + C' with the dot; A B is a missing operator; and A ^ B is rejected rather than silently read as a power or a XOR.
Questions
What do the logic symbols ∧, ∨ and ¬ mean?
And, or and not. p ∧ q is true when both p and q are, p ∨ q when at least one is, and ¬p when p is false.
What is the symbol for “therefore” in logic?
∴, three dots in a triangle. In LaTeX it is \therefore (amssymb) and in HTML ∴.
What is the difference between → and ⇒?
Many books use → for the connective inside a formula and ⇒ to say that one statement implies another; others use the two interchangeably. Both are read “implies”.
What is the difference between ⊢ and ⊨?
⊢ is about proof: the conclusion can be derived from the premises by rules. ⊨ is about truth: the conclusion is true whenever the premises are. For propositional logic the two agree.
Is ~ the same as ¬?
In logic textbooks, yes: both mean not. In C, Java and JavaScript ~ flips every bit of a number instead, which is why Tangibool’s tools ask for NOT, ! or ¬.
How do I type logic symbols in Word?
Insert › Symbol, or in Word for Windows type the Unicode code and press Alt+X (2227 then Alt+X gives ∧), or type commands such as \wedge and \neg followed by a space inside an equation.
Which notation does the engine print by default?
The one you choose: words, programming, mathematical or algebra. Each page of this reference prints every formula in all four, and the fully bracketed form on the precedence page shows the grouping.
Can I use the overbar for NOT?
Not on input; type NOT A, !A, ¬A or A'. The LaTeX export writes negation as an overbar, which is the common algebra typography.
Related
Guides
See also
- Operator precedence in Boolean logic: NOT, then AND, then XOR, then OR
- “=” is not a Boolean operator: use ↔ or compare the formulas
- ^ means XOR in C, Java and Python, not AND or power
- Single & and | are bitwise in most languages
- ~ is bitwise NOT in code, logical NOT in some textbooks
- Arrow variants: => and <=> vs → and ↔, which means what
- AB is one name, not A AND B: implicit multiplication
- Boolean logic in Python: and, or, not, precedence and common mistakes
- Boolean logic in LaTeX: \land, \lor, \lnot and truth tables
Languages
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.