Elementary logic and set theory

Table of contents: Logical operations - Sets - Set operations

Logical operations

Symbol: Not —

\operatorname{not} \left(x\right)

— 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, Ellipsis), rendered as

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

, represents the finite set containing the given elements. In particular, Set() or

\left\{\right\}

is the empty set, and Set(x) or

\left\{x\right\}

is a singleton set.

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, Ellipsis)), ", rendered as", Set(x, y, Ellipsis), ", represents the finite set containing the given elements.", "In particular, ", SourceForm(Set()), "or", Set(), "is the empty set, and", SourceForm(Set(x)), "or", Set(x), "is a singleton set."))

66ca58

Symbol: SetBuilder —

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

— Set comprehension

Called with 3 arguments SetBuilder(f(x), x, P(x)), rendered as

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

, represents the set of values

f\!\left(x\right)

for all

x

satisfying the predicate

P\!\left(x\right)

The argument x to this operator defines a locally bound variable. The corresponding predicate

P\!\left(x\right)

must define the domain of

x

unambiguously; that is, it must include a statement such as

x \in S

where

S

is a known set. More generally, x can be a collection of variables

\left(x, y, \ldots\right)

all of which become locally bound, with a corresponding predicate

P\!\left(x, y, \ldots\right)

Definitions:

Fungrim symbol	Notation	Short description
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension

Source code for this entry:

Entry(ID("66ca58"),
    SymbolDefinition(SetBuilder, SetBuilder(f(x), x, P(x)), "Set comprehension"),
    Description("Called with 3 arguments", SourceForm(SetBuilder(f(x), x, P(x))), ", rendered as", SetBuilder(f(x), x, P(x)), ", represents the set of values", f(x), "for all", x, "satisfying the predicate", P(x), "."),
    Description("The argument", SourceForm(x), "to this operator defines a locally bound variable.", "The corresponding predicate", P(x), "must define the domain of", x, "unambiguously; that is, it must include a statement such as", Element(x, S), "where", S, "is a known set.", "More generally,", SourceForm(x), "can be a collection of variables", Tuple(x, y, Ellipsis), "all of which become locally bound, with a corresponding predicate", P(x, y, Ellipsis), "."))

Set operations

81efd5

Symbol: Cardinality —

\left|S\right|

— Set cardinality

Cardinality(S), rendered as

\left|S\right|

, 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,

\left|\mathbb{Z}\right|

is the cardinality of any countable set and

\left|\mathbb{R}\right|

is the cardinality of the continuum.

Definitions:

Fungrim symbol	Notation	Short description
`Cardinality`	$\left\|S\right\|$	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}\!\left(S\right)

— Power set

Definitions:

Fungrim symbol	Notation	Short description
`PowerSet`	$\mathscr{P}\!\left(S\right)$	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"))