Hubbry Logo
List of logic symbolsList of logic symbolsMain
Open search
List of logic symbols
Community hub
List of logic symbols
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
List of logic symbols
List of logic symbols
List of logic symbols
View on Wikipedia
from Wikipedia
This article contains logic symbols. Without proper rendering support, you may see question marks, boxes, or other symbols instead of logic symbols.

In logic, a set of symbols is commonly used to express logical representation. The following table lists many common symbols, together with their name, how they should be read out loud, and the related field of mathematics. Additionally, the subsequent columns contains an informal explanation, a short example, the Unicode location, the name for use in HTML documents,[1] and the LaTeX symbol.

Basic logic symbols

[edit]
Symbol Unicode
value
(hexadecimal) 		HTML
codes 		LaTeX
symbol 		Logic Name Read as Category Explanation Examples
⇒
→
⊃
 U+21D2

U+2192

U+2283 		⇒
→
⊃

⇒
→
⊃

\Rightarrow
\implies
\to or \rightarrow
\supset
 material conditional (material implication) implies,
if P then Q,
it is not the case that P and not Q 		propositional logic, Boolean algebra, Heyting algebra is false when A is true and B is false but true otherwise.

In other mathematical contexts, see glossary of mathematical symbols, may indicate the domain and codomain of a function and may mean superset.
is true, but is in general false
(since x could be −2).
⇔
↔
≡
 U+21D4

U+2194

U+2261 		⇔
↔
≡

⇔
↔
≡

\Leftrightarrow
\iff
\leftrightarrow
\equiv 		material biconditional (material equivalence) if and only if, iff, xnor propositional logic, Boolean algebra is true only if both A and B are false, or both A and B are true. Whether a symbol means a material biconditional or a logical equivalence, depends on the author’s style.
¬
~
!

′

U+00AC

U+007E

U+0021

U+2032 		¬
˜
!
′

¬
˜
!
′

\lnot or \neg

\sim


' 		negation not propositional logic, Boolean algebra The statement is true if and only if A is false.

A slash placed through another operator is the same as placed in front.

The prime symbol is placed after the negated thing, e.g. [2]


∧
·
&
 U+2227

U+00B7

U+0026 		∧
·
&

∧
·
&
\wedge or \land
\cdot

\&[3]
 logical conjunction and propositional logic, Boolean algebra The statement A ∧ B is true if A and B are both true; otherwise, it is false.
n < 4  ∧  n >2  ⇔  n = 3 when n is a natural number.
∨
+
∥
 U+2228

U+002B

U+2225 		&#8744;
&#43;
&#8741;

&or;
&plus;
&parallel;

\lor or \vee



\parallel 		logical (inclusive) disjunction or propositional logic, Boolean algebra The statement A ∨ B is true if A or B (or both) are true; if both are false, the statement is false.
n ≥ 4  ∨  n ≤ 2  ⇔ n ≠ 3 when n is a natural number.

⊕
⊻
↮
≢
 U+2295

U+22BB

U+21AE

U+2262 		&#8853;
&#8891;
&#8622;
&#8802;

&oplus;
&veebar;
—
&nequiv;

\oplus

\veebar



\not\equiv 		exclusive disjunction xor,
either ... or ... (but not both) 		propositional logic, Boolean algebra The statement is true when either A or B, but not both, are true. This is equivalent to
¬(A ↔ B), hence the symbols and .
is always true and is always false (if vacuous truth is excluded).

⊤
T
1

U+22A4





 &#8868;


&top;

 \top



 true (tautology) top, truth, tautology, verum, full clause propositional logic, Boolean algebra, first-order logic denotes a proposition that is always true.
The proposition is always true since at least one of the two is unconditionally true.

⊥
F
0

U+22A5





 &#8869;

&perp;



 \bot



 false (contradiction) bottom, falsity, contradiction, falsum, empty clause propositional logic, Boolean algebra, first-order logic denotes a proposition that is always false.
The symbol ⊥ may also refer to perpendicular lines.
The proposition is always false since at least one of the two is unconditionally false.
∀
()
 U+2200


 &#8704;

&forall;


 \forall


 universal quantification given any, for all, for every, for each, for any first-order logic   or
  says “given any , has property .”
∃
 U+2203 &#8707;

&exist;

\exists existential quantification there exists, for some first-order logic   says “there exists an (at least one) such that has property .”
n is even.
∃!
 U+2203 U+0021 &#8707; &#33;

&exist;!

\exists ! uniqueness quantification there exists exactly one first-order logic (abbreviation) says “there exists exactly one such that has property .” Only and are part of formal logic.
is an abbreviation for
( )
 U+0028 U+0029 &#40; &#41;

&lpar;
&rpar;

( ) precedence grouping parentheses; brackets almost all logic syntaxes, as well as metalanguage Perform the operations inside the parentheses first.
(8 ÷ 4) ÷ 2 = 2 ÷ 2 = 1, but 8 ÷ (4 ÷ 2) = 8 ÷ 2 = 4.
 U+1D53B &#120123;

&Dopf;

\mathbb{D} domain of discourse domain of discourse metalanguage (first-order logic semantics)
⊢
 U+22A2 &#8866;

&vdash;

\vdash syntactic consequence proves, syntactically entails

(single) turnstile

metalanguage (metalogic) says “ is
a theorem of ”.
In other words,
proves via a deductive system.

(eg. by using natural deduction)
⊨
 U+22A8 &#8872;

&vDash;

\vDash, \models semantic consequence

or satisfaction

(semantically) entails

or satisfies, models double turnstile

metalanguage (metalogic) says
“in every model,
it is not the case that is true and is false”.

says
a formula

is true in a model with

variable assignment .


(eg. by using truth tables)
≡
⟚
⇔
 U+2261

U+27DA

U+21D4 		&#8801;

—
&#8660; &equiv; — &hArr;

\equiv



\Leftrightarrow 		logical equivalence is logically equivalent to metalanguage (metalogic) It’s when and . Whether a symbol means a material biconditional or a logical equivalence, depends on the author’s style.
⊬
 U+22AC ⊬\nvdash does not syntactically entail (does not prove) metalanguage (metalogic) says “ is
not a theorem of ”.
In other words,
is not derivable from via a deductive system.
⊭
 U+22AD ⊭\nvDash does not semantically entail metalanguage (metalogic) says “ does not guarantee the truth of  ”.
In other words,
does not make true.
□
 U+25A1 \Box necessity (in a model) box; it is necessary that modal logic modal operator for “it is necessary that”
in alethic logic, “it is provable that”
in provability logic, “it is obligatory that”
in deontic logic, “it is believed that”
in doxastic logic.
says “it is necessary that everything has property ”
◇
 U+25C7 \Diamond possibility (in a model) diamond;
it is possible that 		modal logic modal operator for “it is possible that”, (in most modal logics it is defined as “¬□¬”, “it is not necessarily not”).
says “it is possible that something has property ”
∴
 U+2234 ∴\therefore therefore therefore metalanguage abbreviation for “therefore”.
∵
 U+2235 ∵\because because because metalanguage abbreviation for “because”.
≔
≜
≝
 U+2254

U+225C

U+225D 		&#8788;

&coloneq;

≔ \coloneqq

:=

\triangleq


\stackrel{

\scriptscriptstyle \mathrm{def}}{=}

definition is defined as metalanguage means "from now on, is defined to be another name for ." This is a statement in the metalanguage, not the object language. The notation may occasionally be seen in physics, meaning the same as .
↑
|

⊼

U+2191
U+007C

U+22BC

\uparrow Sheffer stroke, NAND NAND, not both

up arrow

Propositional logic NAND is the negation of conjunction so is true if and only if it's not the case that both A and B are true.

See also NAND gate

↓

⊽

U+2193

U+22BC

\downarrow Peirce Arrow,
NOR 		nor

down arrow

Propositional logic NOR is the negation of conjunction so is true if and only if both A and B are false.

See also NOR gate

Advanced or rarely used logical symbols

[edit]

The following symbols are either advanced and context-sensitive or very rarely used:

Symbol Unicode
value
(hexadecimal) 		HTML
value
(decimal) 		HTML
entity
(named) 		LaTeX
symbol 		Logic Name Read as Category Explanation
⥽
 U+297D \strictif right fish tail Sometimes used for “relation”, also used for denoting various ad hoc relations (for example, for denoting “witnessing” in the context of Rosser's trick). The fish tail is also used as strict implication by C.I.Lewis ⥽ .
̅
 U+0305 combining overline Used format for denoting Gödel numbers. Using HTML style “4̅” is an abbreviation for the standard numeral “SSSS0”.

It may also denote a negation (used primarily in electronics).

⌜
⌝
 U+231C
U+231D 		\ulcorner

\urcorner

top left corner
top right corner 		Corner quotes, also called “Quine quotes”; for quasi-quotation, i.e. quoting specific context of unspecified (“variable”) expressions;[4] also used for denoting Gödel number;[5] for example “⌜G⌝” denotes the Gödel number of G. (Typographical note: although the quotes appears as a “pair” in unicode (231C and 231D), they are not symmetrical in some fonts. In some fonts (for example Arial) they are only symmetrical in certain sizes. Alternatively the quotes can be rendered as ⌈ and ⌉ (U+2308 and U+2309) or by using a negation symbol and a reversed negation symbol ⌐ ¬ in superscript mode.)
∄
 U+2204 \nexists there does not exist Strike out existential quantifier. “¬∃” used some times instead.
⊙
 U+2299 \odot circled dot operator A sign for the XNOR operator (material biconditional and XNOR are the same operation).
⟛
 U+27DB left and right tack “Proves and is proved by”.
⊩
 U+22A9 forces One of this symbol’s uses is to mean “truthmakes” in the truthmaker theory of truth. It is also used to mean “forces” in the set theory method of forcing.
⟡
 U+27E1 white concave-sided diamond never modal operator
⟢
 U+27E2 white concave-sided diamond with leftwards tick was never modal operator
⟣
 U+27E3 white concave-sided diamond with rightwards tick will never be modal operator
⟤
 U+25A4 white square with leftwards tick was always modal operator
⟥
 U+25A5 white square with rightwards tick will always be modal operator
⋆
 U+22C6 star operator May sometimes be used for ad-hoc operators.
⌐
 U+2310 reversed not sign
⨇
 U+2A07 two logical AND operator

See also

[edit]

References

[edit]

Further reading

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

List of logic symbols

View on Grokipedia
from Grokipedia
A list of logic symbols comprises the standardized graphical notations utilized in mathematical logic to represent fundamental operations, relations, and quantifiers that structure formal arguments and propositions. These symbols form the core vocabulary of formal systems, enabling the precise articulation of logical relationships without reliance on ambiguity. Essential examples include connectives for propositional logic—such as (¬, meaning "not"), conjunction (∧, meaning "and"), disjunction (∨, meaning "or"), material implication (→, meaning "if...then"), and biconditional (↔, meaning "if and only if")—alongside quantifiers for predicate logic, like the universal quantifier (∀, meaning "for all") and existential quantifier (∃, meaning "there exists"). Such symbols are categorized primarily by the branch of logic they serve: propositional logic symbols handle truth-functional compounds of atomic statements, predicate logic extends this with quantifiers and predicates to address objects and properties, while advanced variants appear in (e.g., necessity □ and possibility ◇) and (e.g., membership ∈ and subset ⊂). Their role is pivotal in evaluating the validity of arguments through truth tables and semantic models, underpinning applications in , , and . Standardization of these notations, including the widespread adoption of many current forms, occurred in the early through works like and Alfred North Whitehead's Principia Mathematica (1910–1913), which built on earlier innovations by (1847) and (1889). The evolution of logic symbols traces back to 19th-century efforts to algebraize reasoning, with Augustus De Morgan introducing relational notations like X)Y for categorical statements in 1847, and Ernst Schröder employing ⊂ for subordination in 1890. Today, while some alternative notations persist (e.g., ~ for negation or & for conjunction in certain contexts), the symbols listed in formal references ensure interoperability across logical frameworks, facilitating rigorous proof construction and automated reasoning in digital systems.

Symbols in Propositional Logic

Negation and Unary Operators

In propositional logic, is a fundamental unary operator that reverses the of a single . The standard symbol for is ¬, pronounced "not," and it is applied to a pp to form the ¬p¬p, which is true if pp is false and false if pp is true. This operator plays a central syntactic role in building complex by inverting the logical value of atomic propositions without requiring additional operands. The truth-functional behavior of is captured in its , which demonstrates its exhaustive inversion:
pp¬p¬p
TrueFalse
FalseTrue
This table illustrates that is a total function on truth values, ensuring every yields a determinate opposite. As defined in classical propositional logic, satisfies the law of , where ¬¬p¬¬p is logically equivalent to pp, reinforcing its role as an involution. Alternative notations for negation have been used historically, particularly in early 20th-century logic texts. For instance, the tilde symbol ~, as in ~p, was employed by philosophers like in Principia Mathematica (1910–1913) to denote denial or negation, reflecting a convention borrowed from algebraic traditions. Similarly, the overline ¯, as in ¯p, has been used in some early 20th-century logic texts and later in for negation, often for compactness in printed formulas, though ¬ gradually became the dominant by mid-century due to its clarity in typewriting and printing. These variants underscore the evolution of symbolic notation toward standardization in formal logic.

Binary Connectives

Binary connectives in propositional logic are operators that combine two s to form a new compound , serving as the foundational building blocks for expressing complex logical relationships. These connectives are truth-functional, meaning the truth of the resulting depends solely on the truth s of its operands. The primary binary connectives include conjunction, disjunction, material implication, and biconditional, each with standardized symbols and interpretations established in .

Conjunction (∧)

The conjunction connective, denoted by the symbol ∧ (pronounced "and"), yields a true only when both operands are true. For s pp and qq, the p∧qp \wedge q is true if both pp and qq hold, otherwise false; this captures the intuitive notion of simultaneous truth, as in "It is raining and it is cold." The for conjunction is as follows:
ppqqp∧qp \wedge q
TTT
TFF
FTF
FFF
This connective was employed in early formal systems, including Russell and Whitehead's , where conjunction was represented by a centered dot (·).

Disjunction (∨)

Disjunction, symbolized by ∨ (pronounced "or"), results in a true proposition if at least one operand is true, and false only if both are false. The expression p∨qp \vee q exemplifies inclusive disjunction, true in cases where either or both propositions are true, such as "It is raining or it is cold" (allowing for both conditions). This is the standard interpretation in propositional logic, though exclusive variants (true only when exactly one operand is true) exist in other contexts like digital circuits. Its truth table is:
ppqqp∨qp \vee q
TTT
TFT
FTT
FFF
Disjunction appeared in Principia Mathematica using the modern symbol ∨.

Material Implication (→)

Material implication, denoted → (pronounced "implies" or ""), is false only when the antecedent is true and the consequent is false; it is true in all other cases. For p→qp \rightarrow q, this models conditional reasoning, as in "If it is raining, then it is cold," where the falsehood arises solely from a true leading to a false conclusion. The material conditional was first described by of in antiquity. The symbol → was introduced by in 1922 and is prominently featured in modern logic, while Principia Mathematica used ⊃. The is:
ppqqp→qp \rightarrow q
TTT
TFF
FTT
FFT
In older texts, ⊃ serves as an alternative to →.

Biconditional (↔)

The biconditional, represented by ↔ (pronounced ""), is true when both operands have the same and false otherwise. The formula p↔qp \leftrightarrow q indicates equivalence, true if both are true or both false, and is logically equivalent to (p→q)∧(q→p)(p \rightarrow q) \wedge (q \rightarrow p). An example is "It is raining it is cold," emphasizing mutual dependence. Its truth table is:
ppqqp↔qp \leftrightarrow q
TTT
TFF
FTF
FFT
In Principia Mathematica and subsequent older literature, ≡ denotes the biconditional.

Propositional Variables and Constants

In propositional logic, propositional variables serve as the fundamental atomic components, acting as placeholders for simple statements or propositions that can each be assigned one of two truth values: true or false. These variables are conventionally denoted by lowercase letters such as p,q,rp, q, r, following a standard notational practice that distinguishes them from more complex formulas. There exists a countably infinite supply of such variables, allowing for the representation of arbitrarily many distinct atomic propositions without limitation. The truth constant ⊤\top (also known as "") represents a proposition that is invariably true, serving as a universal truth in logical expressions. For instance, the expression p∨⊤p \lor \top is a tautology, always evaluating to true regardless of the of pp, which underscores ⊤\top's role in capturing necessary truths within formal semantics. Similarly, the truth constant ⊥\bot (or "bottom") denotes a proposition that is always false, embodying inherent contradictions in the system. An example is p∧⊥p \land \bot, which simplifies to falsehood for any assignment to pp, highlighting ⊥\bot's utility in expressing impossible or contradictory statements. In some logical systems and notations, particularly in truth tables or informal contexts, the constants true and false are represented as TT and FF, respectively. These symbols are semantically equivalent to ⊤\top and ⊥\bot in formal propositional logic, where TT always holds true and FF always false, ensuring consistency across interpretive frameworks. Propositional variables and these constants form the basic building blocks that can be combined via connectives to construct compound propositions.

Symbols in First-Order Logic

Quantifiers

In first-order logic, quantifiers are unary operators that bind variables to express generalizations over a domain of discourse, enabling statements about all or some elements satisfying a predicate. The universal quantifier and existential quantifier form the core of this mechanism, with their scope determining the variables they bind and their semantics defining truth conditions relative to a non-empty domain. The universal quantifier, denoted by the symbol ∀ and pronounced "for all," binds a variable such as x in a formula like ∀x P(x)\forall x \, P(x), asserting that the predicate P holds for every element x in the domain. Semantically, ∀x P(x)\forall x \, P(x) is true in a structure if, for every possible assignment of an element from the domain to x, the predicate P(x) evaluates to true, meaning there are no counterexamples in the domain. The symbol ∀ was introduced by Gerhard Gentzen in 1935 as an inverted A (from the German all), by analogy with the existential quantifier symbol. The existential quantifier, denoted by the symbol ∃ and pronounced "there exists," binds a variable such as x in a like ∃x P(x)\exists x \, P(x), asserting that there is at least one element x in the domain for which the predicate P holds. Semantically, ∃x P(x)\exists x \, P(x) is true in a if there exists at least one assignment of an element from the domain to x such that P(x) evaluates to true. The symbol ∃ was introduced by in 1889 in his Arithmetices principia, representing the initial letters of the Latin exi(s)tit. Bounded quantifiers restrict the scope of quantification to a of the domain, typically a set S, using notation such as ∀x∈S P(x)\forall x \in S \, P(x) for over S or ∃x∈S P(x)\exists x \in S \, P(x) for existential. This is semantically equivalent to ∀x(x∈S→P(x))\forall x (x \in S \to P(x)) or ∃x(x∈S∧P(x))\exists x (x \in S \land P(x)), respectively, thereby limiting the domain to elements of S and avoiding quantification over the entire ; variations include (∀x:S)P(x)(\forall x : S) P(x) or ∀x∈S:P(x)\forall x \in S : P(x), depending on notational conventions. Every in can be transformed into an equivalent , where all quantifiers are pulled to the front, prefixed to a quantifier-free matrix. For instance, the P(x)→∀y Q(y)P(x) \to \forall y \, Q(y) (with x not free in Q) can be rewritten as ∀y(P(x)→Q(y))\forall y (P(x) \to Q(y)), moving the universal quantifier outside while preserving equivalence.

Predicates and Functions

In , predicate symbols represent relations or properties among objects in the , each specified by an indicating the number of arguments it accepts. Unary predicates, such as P(x)P(x), denote properties of individual objects, like "is even" applied to a number xx. Binary predicates, such as R(x,y)R(x, y), express relations between two objects, for instance "is greater than" where R(x,y)R(x, y) holds if x>yx > y. Higher-arity predicates extend this to multiple arguments, while 0-ary predicates function as propositional constants that evaluate to true or false without arguments, bridging propositional and predicate logic. Function symbols denote mappings from objects to other objects, also characterized by arity, and are used to construct complex terms through nested application. A unary function symbol f(x)f(x) maps a single input to an output, such as "successor of" where f(x)f(x) yields the next after xx. Binary functions like g(x,y)g(x, y) take two inputs, exemplified by where g(x,y)=x+yg(x, y) = x + y. Terms are built recursively, as in f(g(x))f(g(x)), which first applies gg to xx and then ff to the result, enabling the expression of structured references within formulas. The equality symbol == serves as a distinguished binary predicate denoting identity between terms, where x=yx = y asserts that xx and yy refer to the same object. In logical theories incorporating equality, it satisfies reflexivity (∀x(x=x)\forall x (x = x)), (∀x∀y(x=y→y=x)\forall x \forall y (x = y \to y = x)), and transitivity (∀x∀y∀z(x=y∧y=z→x=z)\forall x \forall y \forall z (x = y \land y = z \to x = z)), forming an on the domain. Within predicate applications, variables exhibit free or bound occurrences depending on their scope relative to quantifiers, which bind variables in formulas. For example, in ∀x P(x,y)\forall x \, P(x, y), the variable xx is bound by the universal quantifier, while yy remains free, allowing substitution or valuation of yy independently of the quantification over xx. This distinction ensures precise interpretation, as free variables act as placeholders for arbitrary domain elements, whereas bound ones range over the entire domain.

Terms and Variables

In , individual variables, typically denoted by lowercase letters such as xx, yy, or zz, serve as placeholders for objects in the . These variables can be free or bound depending on their occurrence in a ; a variable is free if it is not within the scope of a quantifier, as in the P(x)P(x) where xx remains unbound, allowing it to take any value from the domain. In contrast, a variable becomes bound when it falls under a quantifier's scope, such as in ∀x P(x)\forall x \, P(x), where xx is no longer a free placeholder but is universally quantified over the domain. The distinction between free and bound variables is crucial for determining the logical structure and truth conditions of formulas, as free variables function like parameters while bound ones express generality. Constant symbols, often represented by lowercase letters like aa, bb, or cc, denote specific objects in the domain and are treated as 0-ary function symbols, forming simple terms on their own, such as aa. These constants can combine with other elements, for instance, appearing as arguments in more complex expressions like f(a)f(a), where they provide fixed referents without variability. Terms in are built recursively from variables and constants using function symbols. The base cases include every variable and every constant as a term; for compound terms, if ff is an nn-ary function symbol and t1,…,tnt_1, \dots, t_n are terms, then f(t1,…,tn)f(t_1, \dots, t_n) forms a new term, such as f(x,g(y))f(x, g(y)) where g(y)g(y) is itself a term. Well-formed terms must adhere to this inductive definition, ensuring proper matching—each function symbol applied to exactly the correct number of subterms—and avoiding undefined or mismatched constructions to maintain syntactic validity. Terms serve as arguments to predicates, filling roles in atomic formulas like P(t)P(t). Substitution is a key operation for replacing free occurrences of a variable in a formula with a term, denoted as P(t/x)P(t/x) to indicate substituting term tt for variable xx in formula P(x)P(x). This process must avoid variable capture, where a substituted term introduces a variable that could bind unintended parts of the formula, often requiring prior adjustments. Alpha-equivalence addresses the renaming of bound variables, stating that two formulas are equivalent if one can be obtained from the other by consistently replacing bound variables without altering the formula's meaning, such as ∀x P(x)\forall x \, P(x) being alpha-equivalent to ∀y P(y)\forall y \, P(y). This treatment ensures that logical properties remain invariant under such renamings, facilitating proofs and normal forms in .

Symbols in Set Theory

Membership and Subset Relations

In set theory, the membership relation is denoted by the symbol ∈, a binary predicate where x ∈ A indicates that x is an element of the set A. This symbol serves as the foundational primitive predicate in Zermelo-Fraenkel set theory (ZF), the standard axiomatic framework for set theory, allowing the construction of all mathematical objects from sets via membership. The non-membership relation is symbolized by ∉, defined as the negation of membership: x ∉ A if and only if ¬(x ∈ A). This relation is essential in defining the empty set ∅, the unique set with no elements, formalized in ZF's Axiom of the Empty Set as the existence of a set such that ∀x (x ∉ ∅). The relation is denoted by ⊆, where A ⊆ B means that every element of A is also an element of B, formally expressed as ∀x (x ∈ A → x ∈ B). This includes the case where A = B, making ⊆ reflexive. The proper relation uses ⊂, defined as A ⊂ B if A ⊆ B and A ≠ B, emphasizing strict inclusion without equality. These relations capture the hierarchical structure of sets, originating conceptually in Georg Cantor's foundational work on in the late 19th century, with notation such as ⊂ introduced by in and Ernst Schröder in 1890. The superset relations are the converses: B ⊇ A means A ⊆ B, so B contains all elements of A (possibly equal), while B ⊃ A means A ⊂ B, indicating strict . For example, if A = {1, 2} and B = {1, 2, 3}, then A ⊆ B, A ⊂ B, B ⊇ A, and B ⊃ A. These symbols, like their counterparts, evolved from Cantor's ideas on point sets and inclusions but were formalized in symbolic logic by Schröder and Peano to facilitate rigorous proofs in .

Set Operations

In set theory, operations on sets provide the foundational means for constructing and manipulating collections of elements, mirroring Boolean operations in logic. These symbols enable the expression of unions, intersections, and other combinations that form the basis for more complex mathematical structures. The following outlines key symbols used for these operations, emphasizing their definitions, properties, and applications within logical frameworks. The union symbol, denoted by ∪\cup, represents the operation that combines two sets AA and BB into a new set containing all elements that belong to AA or BB (or both). Formally, A∪B={x∣x∈A∨x∈B}A \cup B = \{ x \mid x \in A \lor x \in B \}. For example, {1}∪{2}={1,2}\{1\} \cup \{2\} = \{1, 2\}. This operation is commutative, meaning A∪B=B∪AA \cup B = B \cup A. The symbol, denoted by ∩\cap, denotes the set of elements common to both AA and BB. Thus, A∩B={x∣x∈A∧x∈B}A \cap B = \{ x \mid x \in A \land x \in B \}. It exhibits , as A∩A=AA \cap A = A. Additionally, intersection relates to complements via De Morgan's laws, where the complement of the union of two sets equals the intersection of their complements: (A∪B)c=Ac∩Bc(A \cup B)^c = A^c \cap B^c. Set difference, symbolized by ∖\setminus (or sometimes −-), extracts from set AA those elements not present in set BB, defined as A∖B={x∈A∣x∉B}A \setminus B = \{ x \in A \mid x \notin B \}. For instance, if A={1,2}A = \{1, 2\} and B={2}B = \{2\}, then A∖B={1}A \setminus B = \{1\}. This operation is asymmetric, as A∖B≠B∖AA \setminus B \neq B \setminus A in general. The power set of a set AA, denoted P(A)\mathcal{P}(A) or 2A2^A, is the set comprising all possible subsets of AA. Its cardinality is 2∣A∣2^{|A|}, reflecting the exponential growth in the number of subsets as the size of AA increases; this follows from Cantor's theorem, which establishes that ∣P(A)∣>∣A∣|\mathcal{P}(A)| > |A|. In higher-order logics, the power set plays a crucial role by facilitating quantification over subsets, enabling the modeling of predicates and relations as sets of elements. The , symbolized by ∅\emptyset or {}\{\}, is the unique set containing no elements, axiomatized in Zermelo-Fraenkel (ZF) by the of the empty set, which asserts the existence of a set with no members. It satisfies absorption properties such as A∪∅=AA \cup \emptyset = A for any set AA.

Symbols in Modal and Non-Classical Logics

In , operators extend the expressiveness of propositional logic by qualifying statements with notions of necessity and possibility, applying to propositional formulas to express modal concepts across possible s. The necessity operator, denoted by the box symbol □\square (read as "necessarily"), asserts that a pp holds in all worlds accessible from the current world in a Kripke frame, a semantic structure consisting of a set of possible worlds equipped with an accessibility relation. For example, □p\square p is true at a world ww if pp is true at every world vv such that wRvwRv, where RR is the accessibility relation. A key characterizing necessity in normal modal logics is the distribution K: □(p→q)→(□p→□q)\square(p \to q) \to (\square p \to \square q), which ensures that necessity preserves implication. Dually, the possibility operator, denoted by the diamond symbol ◊\Diamond (read as "possibly"), is defined as ◊p≡¬□¬p\Diamond p \equiv \neg \square \neg p and holds if there exists at least one accessible world where pp is true, analogous to an existential quantifier over accessible worlds. This duality allows possibility to be interdefinable with necessity, enabling derivations such as ◊p→□◊p\Diamond p \to \square \Diamond p in certain systems based on properties of the accessibility relation. The historical development of these operators traces back to Clarence Irving Lewis's 1918 introduction of strict implication as a modal alternative to material implication, motivated by the desire to capture that holds necessarily rather than contingently; strict implication p≺qp \prec q was later formalized using necessity as □(p→q)\square(p \to q). Lewis's work culminated in the 1932 systems S1 through S5, which varied in strength based on governing necessity. Saul Kripke's 1963 possible worlds semantics provided a rigorous model-theoretic foundation via Kripke frames, where the accessibility relation's properties correspond to modal : reflexivity for axiom T (□p→p\square p \to p), transitivity for axiom 4 (□p→□□p\square p \to \square \square p), and euclideaness (or seriality combined with symmetry) for axiom 5 (◊p→□◊p\Diamond p \to \square \Diamond p), yielding the standard systems K (basic), T (reflexive), S4 (reflexive and transitive), and S5 (). In multi-modal logics, operators are indexed to distinguish different modalities, such as □ip\square_i p for necessity with respect to the ii-th accessibility relation, allowing simultaneous modeling of alethic necessity alongside epistemic modalities (e.g., as □kp\square_k p, true in all worlds compatible with an agent's ) or deontic modalities (e.g., as □op\square_o p, true in all ideal worlds). These indexed enable the of interactions between modalities, as in hybrid epistemic-deontic systems.

Specialized Non-Classical Symbols

In non-classical logics, specialized symbols extend beyond classical bivalent semantics to capture temporal dynamics, constructive proofs, graduated truth values, and resource-sensitive reasoning. These notations deviate from classical principles such as the or unrestricted reusability of assumptions, enabling formalization of phenomena like program verification, computational proofs, and uncertain knowledge. Temporal operators in (LTL) and its past extensions address sequences of states over time. LTL, introduced by Amir Pnueli to verify reactive systems, is future-oriented. The operator GG denotes "globally" or "always in the future," meaning a pp holds in all subsequent states, as in GpGp, which asserts pp is true henceforth along the path. Similarly, FF means "eventually," indicating pp will hold at some future state. For past-oriented reasoning in extensions like past LTL, HH signifies "historically" or "always in the past," and PP denotes "previously," referring to the immediate prior state. These unary operators prefix propositions and form the basis for in . Intuitionistic logic, formalized by Arend Heyting, rejects classical elimination (¬¬p→p\neg\neg p \to p) and uses implication ⊃\supset with constructive semantics, where p⊃qp \supset q requires a proof of qq from pp, unlike material implication's truth-functional detachment. This symbol operates within Heyting algebras, which are distributive lattices equipped with a relative pseudocomplement defining p⊃qp \supset q as the largest element implying qq when conjoined with pp, providing a semantic foundation for intuitionistic validity without bivalence. ¬p\neg p is defined as p⊃⊥p \supset \bot, contrasting classical ¬p\neg p by lacking proof without direct disproof of pp. Fuzzy logic accommodates truth values in the continuous interval [0,1], originating from Lotfi A. Zadeh's fuzzy sets to model . The Łukasiewicz implication, a key connective, is defined as p→q=min⁡(1,1−p+q)p \to q = \min(1, 1 - p + q), which generalizes classical implication by measuring the degree to which the truth of pp supports qq; for example, if p=0.7p = 0.7 and q=0.4q = 0.4, then p→q=0.7p \to q = 0.7, reflecting partial entailment. This operator arises from Łukasiewicz's many-valued logics but gains prominence in fuzzy systems for approximate reasoning in control and . Linear logic, developed by Jean-Yves Girard, treats propositions as resources with linear use, distinguishing multiplicative from additive connectives to model non-commutative, consumption-aware inference. The multiplicative conjunction ⊗\otimes (tensor) combines resources in parallel without choice, as in p⊗qp \otimes q, which consumes both pp and qq exactly once, emphasizing scarcity unlike classical ∧\land's reusability. In contrast, the additive disjunction ⊕\oplus offers a choice between pp or qq, with proofs selecting one branch. These symbols enable phase-space semantics and applications in concurrency and , where ⊗\otimes is non-commutative in sequent calculi.

References

  1. https://www.columbia.edu/~jc4345/Symbolic%20Logic%20--%20combined%204.26.24.pdf
  2. https://old.maa.org/press/periodicals/convergence/math-origins-the-logical-symbols
  3. https://plato.stanford.edu/entries/logic-propositional/
  4. https://plato.stanford.edu/entries/pm-notation/
  5. https://plato.stanford.edu/entries/disjunction/
  6. https://mathshistory.st-andrews.ac.uk/Miller/mathsym/set/
  7. https://www.logicinaction.org/docs/ch2.pdf
  8. https://www.sciencedirect.com/topics/computer-science/propositional-variable
  9. https://mathvault.ca/hub/higher-math/math-symbols/logic-symbols/
  10. https://avigad.github.io/lamr/propositional_logic.html
  11. https://web.engr.oregonstate.edu/~afern/GOFAI/notes/first-order-logic-syntax-semantics.pdf
  12. http://www.sci.brooklyn.cuny.edu/~chipp/cis32/lectures/Lecture16.pdf
  13. https://www3.cs.stonybrook.edu/~cse541/Spring2009/cse541PredLogic.pdf
  14. https://www.cs.cornell.edu/courses/cs486/2005sp/lect19.pdf
  15. https://www.cs.cmu.edu/~10606/predlogic.pdf
  16. https://www.cs.rice.edu/~vardi/comp409/lec15.pdf
  17. https://mathworld.wolfram.com/First-OrderLogic.html
  18. https://plato.stanford.edu/entries/logic-classical/
  19. https://plato.stanford.edu/entries/zermelo-set-theory/
  20. https://hsm.stackexchange.com/questions/15913/what-was-the-motivation-for-the-choice-of-the-subset-symbol
  21. https://plato.stanford.edu/entries/set-theory/basic-set-theory.html
  22. https://plato.stanford.edu/entries/set-theory/
  23. https://mathworld.wolfram.com/deMorgansLaws.html
  24. https://plato.stanford.edu/entries/logic-modal/
  25. https://www.filosoficas.unam.mx/~morado/Cursos/17Modal/Kripke1963.pdf
  26. https://iep.utm.edu/lewisci/
  27. https://dl.acm.org/doi/10.1109/SFCS.1977.32
  28. https://plato.stanford.edu/entries/logic-temporal/
  29. https://plato.stanford.edu/entries/logic-intuitionistic/
  30. https://www.sciencedirect.com/science/article/pii/0304397587900454
Add your contribution
Related Hubs
User Avatar
No comments yet.