Logical symbols

List of common symbols used in various logics.

• The verum: $\top$

  • true, top, tee, T

  • tautology, unconditional truth

• The falsum: $\bot$

  • false, bottom, falsity, ⊥

  • contradiction, unconditional falsity, absurdity

• The hook: $\lnot$

  • negation, NOT, ¬

  • logical negation

• The wedge: $\land$

  • ascending wedge, AND, ac, atque, ∧

  • logical conjunction

• The vel: $\lor$

  • descending wedge, OR, vee, v

  • logical disjunction

• The arrow:

  • arrows: $\to$, $\Rightarrow$, $\implies$

  • glyphs: →, ⇒, ⟹

  • read as "implies", "if...then"

  • logical (material) implication

  • bigger arrows may represent higher precedence

• The double arrow:

  • "if and only if"

  • logical biconditional, $\iff$

  • material equivalence, $\Leftrightarrow$,⇔

  • equivalence, $\leftrightarrow$, ↔

  • logical equivalence, $\equiv$, ≡

  • bigger arrows may represent higher precedence

• The turnstile: $\vdash$

  • glyph⊢

  • "right tack", "tee", "assertion sign" symbol

  • "yields", "proves", "satisfies", "entails"

  • symbol for assertion, entailment, implication

  • syntactic consequence

• The double turnstile, $\models$

  • "entails", "models", "makes true", "is stronger than", "is a semantic consequence of", ⊨

  • semantic consequence

  • "A is a model of φ": ⊨A φ

• The for all: $\forall$

  • "for all", ∀

  • universal quantifier

• The there exists: $\exists$

  • "there is", "there exists", ∃

  • existential quantifier

  • unique existential quantifier: ∃!

• Other symbols:

  • "has the same cardinality as": ≈

  • "has smaller cardinality than": ≺

  • "x maps to y" (functions): x ↦ y

The turnstile

• Represents: binary relation, assertion symbol

• Commonly seen in sequent calculus

• Often read as "yields", "proves", "satisfies", "entails"

• Created by Gottlob Frege in 1879

• Judgement of some content e.g. $\vdash A$ could be read as "I know $A$ is true".

• A conditional assertion $P\vdash Q$ could be read as "From $P$, I know that $Q$".

• In proof theory represents provability: if $T$ is a formal theory and $S$ is a particular sentence in the language of the theory then $T\vdash S$ means that $S$ is provable from $T$.

• In the typed lambda calculus the turnstile is used to separate typing assumptions from the typing judgment.

• In category theory, a reversed turnstile, as in $F\dashv G$, is used to indicate that the functor $F$ is left adjoint to the functor $G$. It is rarely used as $F\vdash G$ to indicate that the functor $F$ is right adjoint to the functor $G$.