Set Representations

A set is a collection of distinct objects. There are four common ways to
write one down:

• Enumeration (explicit list): $\{1, 2, 3\}$
• Characteristic function: $f(x) = 1$ if $x \in S$, else $0$
• Set-builder / comprehension: $\{x \mid P(x)\}$ — "the set of all $x$ with property $P$"
• Recursive definition: $\{0\} \cup \{s(n) \mid n \in \mathbb{N}\}$

We assume we can write down any set — this is the (controversial) axiom
of comprehension: every set we can describe exists. (Naïve set theory ignores
the Russell paradox.)

The elements of a set are unordered and unique: $\{1, 2, 3\} = \{3, 2, 1\}$.

Some expressions introduce new variables that range over a domain:

• Universal quantification $\forall x.\, P(x)$ — '$P$ holds for every $x$'.
• Existential quantification $\exists x.\, P(x)$ — 'there exists an $x$ such that $P(x)$'.
• Function definition $f(x) := x^2 + 1$ — '$f$ of $x$ is defined as $x^2 + 1$'.

The introduced variable $x$ is bound by its binder ($\forall, \exists, :=$). The scope of the binding is the smallest enclosing formula. A variable occurrence is free if it is not bound.

Examples:
- $\forall x.\, x + 1 > x$ — $x$ bound by $\forall$, holds for every number.
- $\exists x.\, x^2 = 2$ — $x$ bound by $\exists$, $\sqrt{2}$ exists.
- $\int_0^1 x^2 \, dx$ — $x$ bound by the integral sign.

Renaming bound variables preserves meaning: $\forall x.\, P(x) \equiv \forall y.\, P(y)$.