Elementary logic and set theory

Table of contents: Logical operations - Sets - Set operations

Logical operations

Symbol: Not —

\operatorname{not} x

— Logical not

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("488b6d"),
    SymbolDefinition(Not, Not(x), "Logical not"))

0a6d2e

Symbol: And —

x \;\mathbin{\operatorname{and}}\; y

— Logical and

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("0a6d2e"),
    SymbolDefinition(And, And(x, y), "Logical and"))

a53803

Symbol: Or —

x \;\mathbin{\operatorname{or}}\; y

— Logical or

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("a53803"),
    SymbolDefinition(Or, Or(x, y), "Logical or"))

2d6cf1

Symbol: Equivalent —

\left(x\right) \iff \left(y\right)

— Logical equivalence

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("2d6cf1"),
    SymbolDefinition(Equivalent, Equivalent(x, y), "Logical equivalence"))

379aa0

Symbol: Implies —

\left(x\right) \;\implies\; \left(y\right)

— Logical implication

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("379aa0"),
    SymbolDefinition(Implies, Implies(x, y), "Logical implication"))

Sets

cf447f

Symbol: Set —

\left\{\ldots\right\}

— Set with given elements

Set(x, y, z), rendered as

\left\{x, y, z\right\}

, represents the finite set containing the given elements (and similarly with any number of argumeents). In particular, Set() or {} is the empty set, and Set(x) or

\left\{x\right\}

is a singleton set.

The special expressions For, ForElement define a set comprehension:

Set(f(x), For(x), P(x)), rendered as

\left\{ f(x) : P(x) \right\}

Set(f(x), ForElement(x, S)), rendered as

\left\{ f(x) : x \in S \right\}

Set(f(x), ForElement(x, S), P(x)), rendered as

\left\{ f(x) : x \in S \,\mathbin{\operatorname{and}}\, P(x) \right\}

Set(f(x), For(x, a, b)), rendered as

\left\{f(a), f\!\left(a + 1\right), \ldots, f(b)\right\}

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("cf447f"),
    SymbolDefinition(Set, Set(Ellipsis), "Set with given elements"),
    Description(SourceForm(Set(x, y, z)), ", rendered as", Set(x, y, z), ", represents the finite set containing the given elements (and similarly with any number of argumeents).", "In particular, ", SourceForm(Set()), "or", Set(), "is the empty set, and", SourceForm(Set(x)), "or", Set(x), "is a singleton set."),
    Description("The special expressions", SourceForm(For), ", ", SourceForm(ForElement), "define a set comprehension:"),
    Description(SourceForm(Set(f(x), For(x), P(x))), ", rendered as", Set(f(x), For(x), P(x)), "."),
    Description(SourceForm(Set(f(x), ForElement(x, S))), ", rendered as", Set(f(x), ForElement(x, S)), "."),
    Description(SourceForm(Set(f(x), ForElement(x, S), P(x))), ", rendered as", Set(f(x), ForElement(x, S), P(x)), "."),
    Description(SourceForm(Set(f(x), For(x, a, b))), ", rendered as", Set(f(x), For(x, a, b)), "."))

Set operations

81efd5

Symbol: Cardinality —

\# S

— Set cardinality

Cardinality(S), rendered as

\# S

, represents the cardinality of the set

S

. The cardinality of a finite set is a nonnegative integer. Cardinalities of infinite sets may be represented in terms of this symbol; for example,

\# \mathbb{Z}

is the cardinality of any countable set and

\# \mathbb{R}

is the cardinality of the continuum.

Definitions:

Fungrim symbol	Notation	Short description
`Cardinality`	$\# S$	Set cardinality
`ZZ`	$\mathbb{Z}$	Integers
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("81efd5"),
    SymbolDefinition(Cardinality, Cardinality(S), "Set cardinality"),
    Description(SourceForm(Cardinality(S)), ", rendered as", Cardinality(S), ", represents the cardinality of the set", S, ".", "The cardinality of a finite set is a nonnegative integer.", "Cardinalities of infinite sets may be represented in terms of this symbol;", "for example,", Cardinality(ZZ), "is the cardinality of any countable set", "and", Cardinality(RR), "is the cardinality of the continuum."))

1d963f

Symbol: PowerSet —

\mathscr{P}(S)

— Power set

Definitions:

Fungrim symbol	Notation	Short description
`PowerSet`	$\mathscr{P}(S)$	Power set

Source code for this entry:

Entry(ID("1d963f"),
    SymbolDefinition(PowerSet, PowerSet(S), "Power set"))

985bda

Symbol: Union —

S \cup T

— Set union

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("985bda"),
    SymbolDefinition(Union, Union(S, T), "Set union"))

0e613e

Symbol: Intersection —

S \cap T

— Set intersection

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("0e613e"),
    SymbolDefinition(Intersection, Intersection(S, T), "Set intersection"))

ec33ac

Symbol: SetMinus —

S \setminus T

— Set difference

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("ec33ac"),
    SymbolDefinition(SetMinus, SetMinus(S, T), "Set difference"))

27f845

Symbol: Element —

x \in S

— Set membership

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("27f845"),
    SymbolDefinition(Element, Element(x, S), "Set membership"))

590290

Symbol: NotElement —

x \notin S

— Set non-membership

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("590290"),
    SymbolDefinition(NotElement, NotElement(x, S), "Set non-membership"))

a9e8df

Symbol: Subset —

S \subset T

— Strict subset

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("a9e8df"),
    SymbolDefinition(Subset, Subset(S, T), "Strict subset"))

e58aaf

Symbol: SubsetEqual —

S \subseteq T

— Subset

Definitions:

Fungrim symbol	Notation	Short description

Source code for this entry:

Entry(ID("e58aaf"),
    SymbolDefinition(SubsetEqual, SubsetEqual(S, T), "Subset"))