| ∧ |
Logical AND (Conjunction)
Propositional Logic ($P \land Q$) |
Binary connective outputting true only if both propositions $P$ and $Q$ are simultaneously true. |
Alt 8743 |
U+2227 |
∧ / ∧ |
\land / \wedge |
| ∨ |
Logical OR (Disjunction)
Propositional Logic ($P \lor Q$) |
Binary inclusive connective outputting true if at least one of $P$ or $Q$ is true. |
Alt 8744 |
U+2228 |
∨ / ∨ |
\lor / \vee |
| ¬ |
Logical NOT (Negation)
Propositional Logic ($\neg P$) |
Unary connective reversing the truth value of proposition $P$ ($1 \rightarrow 0, 0 \rightarrow 1$). |
Alt 0172 |
U+00AC |
¬ / ¬ |
\neg / \lnot |
| → |
Material Implication (Conditional)
Conditional ($P \rightarrow Q$) |
"If $P$, then $Q$"; logically equivalent to $\neg P \lor Q$; false only when $P$ is true and $Q$ is false. |
Alt 8594 |
U+2192 |
→ |
\rightarrow |
| ⇒ |
Material Implication Arrow
Formal Implication ($P \implies Q$) |
Double-line arrow denoting logical implication and valid inference deduction. |
Alt 8658 |
U+21D2 |
⇒ |
\implies / \Rightarrow |
| ↔ |
Material Biconditional (IFF)
Biconditional ($P \leftrightarrow Q$) |
"$P$ if and only if $Q$"; true when both $P$ and $Q$ possess identical truth values. |
Alt 8596 |
U+2194 |
↔ |
\leftrightarrow |
| ⇔ |
Logical Equivalence Arrow
Equivalence ($P \iff Q$) |
Denotes strict logical equivalence between two compound propositional formulas. |
Alt 8660 |
U+21D4 |
⇔ |
\iff / \Leftrightarrow |
| ⊕ |
Exclusive OR (XOR)
Modulo-2 Addition ($P \oplus Q$) |
Exclusive disjunction outputting true if either $P$ or $Q$ is true, but false if both are true. |
Alt 8853 |
U+2295 |
⊕ / ⊕ |
\oplus |
| ⊼ |
NAND (Sheffer Stroke)
Universal Connective ($P \mid Q$) |
Negated conjunction outputting false only when both $P$ and $Q$ are true; functionally complete operator. |
Alt 8892 |
U+22BC |
⊼ |
\barwedge |
| ⊽ |
NOR (Peirce Arrow)
Universal Connective ($P \downarrow Q$) |
Negated disjunction outputting true only when both $P$ and $Q$ are false; functionally complete operator. |
Alt 8893 |
U+22BD |
⊽ |
\barvee |
| ≡ |
Logical Equivalence / Identity
Formula Identity ($A \equiv B$) |
Denotes that two logical expressions evaluate to identical truth tables under all valuations. |
Alt 8801 |
U+2261 |
≡ / ≡ |
\equiv |
| ≢ |
Logical Inequivalence
Non-Identity ($A \not\equiv B$) |
Denotes that two expressions have distinct truth assignments. |
Alt 8802 |
U+2262 |
≢ |
\not\equiv |
| ∀ |
Universal Quantifier ("For All")
First-Order Logic ($\forall x$) |
Inverted "A" stating that predicate $P(x)$ holds true for every element $x$ in the domain of discourse. |
Alt 8704 |
U+2200 |
∀ / ∀ |
\forall |
| ∃ |
Existential Quantifier ("There Exists")
First-Order Logic ($\exists x$) |
Reversed "E" stating that predicate $P(x)$ holds true for at least one element $x$ in the domain. |
Alt 8707 |
U+2203 |
∃ / ∃ |
\exists |
| ∄ |
Non-Existence Quantifier ("There Does Not Exist")
First-Order Logic ($\nexists x$) |
Stating that no element $x$ exists in the domain satisfying predicate $P(x)$ ($\neg \exists x P(x)$). |
Alt 8708 |
U+2204 |
∄ |
\nexists |
| ∴ |
Therefore Symbol (Deduction Conclusion)
Formal Deduction |
Three triangular dots placed before the final concluded proposition of a logical argument. |
Alt 8756 |
U+2234 |
∴ / ∴ |
\therefore |
| ∵ |
Because / Since Symbol (Premise)
Formal Argumentation |
Three inverted triangular dots introducing justification or premise statements. |
Alt 8757 |
U+2235 |
∵ |
\because |
| ∎ |
Q.E.D. / Halmos Tombstone (End of Proof)
Mathematical Proofs |
Solid black square marking the completion of a mathematical proof (Quod Erat Demonstrandum). |
Alt 8718 |
U+220E |
∎ |
\blacksquare / \qed |
| ‣ |
Proof Step Bullet (Triangle)
Proof Theory |
Triangular bullet marking sequential proof derivation steps and sub-lemmas. |
Alt 8227 |
U+2023 |
‣ |
\blacktriangleright |
| ⊢ |
Turnstile / Syntactic Provability (Asserts)
Proof Theory ($T \vdash \phi$) |
Syntactic entailment stating formula $\phi$ is provable from axiom set $T$ using inference rules. |
Alt 8866 |
U+22A2 |
⊢ / ⊢ |
\vdash |
| ⊨ |
Double Turnstile / Semantic Entailment (Models)
Model Theory ($M \models \phi$) |
Semantic consequence stating formula $\phi$ is true in all interpretations that satisfy theory $T$. |
Alt 8872 |
U+22A8 |
⊧ / ⊨ |
\models |
| ⊣ |
Reverse Turnstile / Right Assertion
Category Theory & Proofs |
Denotes dual adjunctions or reverse syntactic consequence in sequent calculus. |
Alt 8867 |
U+22A3 |
⊣ |
\dashv |
| ⊬ |
Does Not Prove / Unprovable
Proof Incompleteness |
States that formula $\phi$ cannot be syntactically derived from the given axioms. |
Alt 8876 |
U+22AC |
⊬ |
\nvdash |
| ⊭ |
Does Not Model / Semantic Invalidity
Model Theory |
States that formula $\phi$ is not satisfied by the given model structure. |
Alt 8877 |
U+22AD |
⊭ |
\nvDash |
| ⊤ |
Tautology / Verum / Top Element (True)
Lattice Theory (True) |
Represents universal truth, a proposition that is true in all interpretations, or top lattice element. |
Alt 8868 |
U+22A4 |
⊤ / ⊤ |
\top |
| ⊥ |
Contradiction / Falsum / Bottom Element (False)
Lattice Theory (False) |
Represents an impossible contradiction, a proposition false in all interpretations, or bottom element. |
Alt 8869 |
U+22A5 |
⊥ / ⊥ |
\bot |
| □ |
Necessity Operator (Box)
Modal Logic ($\Box P$) |
"It is necessarily true that $P$"; proposition $P$ holds true in all accessible possible worlds (Kripke semantics). |
Alt 9633 |
U+25A1 |
□ |
\Box / \square |
| ◇ |
Possibility Operator (Diamond)
Modal Logic ($\Diamond P$) |
"It is possibly true that $P$"; proposition $P$ holds true in at least one accessible possible world ($\neg \Box \neg P$). |
Alt 9671 |
U+25C7 |
◇ |
\Diamond / \lozenge |
| ∈ |
Element of / Set Membership
Set Theory ($x \in A$) |
Denotes that element $x$ belongs to set $A$. |
Alt 8712 |
U+2208 |
∈ |
\in |
| ∉ |
Not an Element of
Set Theory ($x \notin A$) |
Denotes that element $x$ does not belong to set $A$. |
Alt 8713 |
U+2209 |
∉ |
\notin |
| ⊆ |
Subset or Equal to
Set Inclusion ($A \subseteq B$) |
Every element of set $A$ is also an element of set $B$. |
Alt 8838 |
U+2286 |
⊆ |
\subseteq |
| ⊂ |
Proper Subset
Set Inclusion ($A \subset B$) |
Set $A$ is contained within set $B$, and $A \neq B$. |
Alt 8834 |
U+2282 |
⊂ |
\subset |
| ∩ |
Set Intersection
Set Theory ($A \cap B$) |
Set of all elements belonging simultaneously to both set $A$ and set $B$. |
Alt 8745 |
U+2229 |
∩ |
\cap |
| ∪ |
Set Union
Set Theory ($A \cup B$) |
Set of all elements belonging to set $A$, set $B$, or both. |
Alt 8746 |
U+222A |
∪ |
\cup |
