# ZFC and first-order logic

Paris

Using a mélange of mathematical syntaxes, we mechanize some exercises from Tao's excellent book

## Ouverture

Let us informally define sets and set membership $\in$. A set is an unordered collection of objects, with the set itself being an object. Set membership checks whether a given object is contained within a set:

\begin{align} \forall x, x \in A \vee x \not\in A \tag{law of excluded middle} \\ A \in C \wedge A = B \rightarrow B \in C \tag{axiom of substitution} \end{align}

The axiom of substition uses the definition of equality:

$$\begin{matrix} A = B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B \\ && \wedge \\ && \forall x, x \in B \rightarrow x \in A \end{matrix}$$

The axiom of substition is preserved for all sets only defined in terms of $\in$ and $=$.

Verify that set equality is reflexive, symmetric, and transitive.

Goal:

$$\begin{matrix} \textrm{reflexive} & \forall A, A = A \\ \textrm{symmetric} & \forall A B, A = B \leftrightarrow B = A \\ \textrm{transitive} & \forall A B C, (A = B) \wedge (B = C) \rightarrow (A = C) \end{matrix}$$

Hypothesis:

$$\begin{matrix} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \end{matrix}$$

Proof.

$$\begin{matrix} A = A & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in A & \textrm{by (eq)} \\ A = B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in A & \\ & \leftrightarrow & B = A & \textrm{by (eq)} \\ A = B &&& \\ \wedge &&& \\ B = C & \rightarrow & \forall x, x \in A \rightarrow x \in B & \textrm{(1)} \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in A & \textrm{(2)} \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in C & \textrm{(3)} \\ && \wedge & \\ && \forall x, x \in C \rightarrow x \in B & \textrm{(4)} \\ & \rightarrow & \forall x, x \in A \rightarrow x \in C & \textrm{by (1) and (3)} \\ && \wedge & \\ && \forall x, x \in C \rightarrow x \in A & \textrm{by (4) and (2)} \\ & \rightarrow & A = C & \textrm{by (eq)} \end{matrix}$$

Qed.

Prove that the following sets are distinct: $\emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \{\emptyset, \{\emptyset\}\}$.

Hypothesis:

\begin{align} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ \forall x, x & \not\in & \emptyset \tag{phi} \\ \forall x, x \in \{a\} & \leftrightarrow & x = a \tag{build-a} \\ \forall x, x \in \{a, b\} & \leftrightarrow & (x = a) \vee (x = b) \tag{build-b} \end{align}

Lemma:

$$\begin{matrix} A \neq B & \leftrightarrow & \exists x, (x \in A \wedge x \not\in B) \vee (x \not\in A \wedge x \in B) & \textrm{by (eq)} \end{matrix}$$

Proof.

$$\begin{matrix} \emptyset & \neq & \textrm{any other set} & \textrm{by (phi) and (eq)} \\ \textrm{Plugging } x = \{\emptyset\} \textrm{ in (lemma)} & \rightarrow & \{\{\emptyset\}\} \neq \{\emptyset\} & \textrm{by (build-a)} \\ \textrm{Plugging } x = \{\emptyset\} \textrm{ in (lemma)} & \rightarrow & \{\emptyset, \{\emptyset\}\} \neq \{\emptyset\} & \textrm{by (build-a) and (build-b)} \\ \textrm{Plugging } x = \emptyset \textrm{ in (lemma)} & \rightarrow & \{\emptyset, \{\emptyset\}\} \neq \{\{\emptyset\}\} & \textrm{by (build-a) and (build-b)} \end{matrix}$$

Qed.

Show that, for any set $A$, $A \cup A = A \cup \emptyset = \emptyset \cup A = A$.

Hypothesis:

\begin{align} A = B \leftrightarrow \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ \forall x, x \in A \cup B \leftrightarrow x \in A \vee x \in B \tag{union} \\ \forall x, x \not\in \emptyset \tag{phi} \end{align}

Proof.

$$\begin{matrix} A \cup A = A & \leftrightarrow \forall x, x \in A \vee x \in A \leftrightarrow x \in A & \textrm{by (eq) and (union)} \\ & \leftrightarrow \forall x, x \in A \leftrightarrow x \in A & \textrm{by intuition} \\ \\ A \cup \emptyset = A & \leftrightarrow \forall x, x \in A \vee x \in \emptyset \leftrightarrow x \in A & \textrm{by (eq) and (union)} \\ & \leftrightarrow \forall x, x \in A \leftrightarrow x \in A & \textrm{by (phi) and intuition} \\ \\ \emptyset \cup A = A && \textrm{by similar argument} \end{matrix}$$

Qed.

Show that, for any three sets $A, B, C$, $A \subseteq B \wedge B \subseteq A \rightarrow A = B$, and $A \subsetneq B \subsetneq C \rightarrow A \subsetneq C$.

Hypothesis:

\begin{align} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ A \neq B & \leftrightarrow & \exists x, (x \in A \wedge x \not\in B) \vee (x \not\in A \wedge x \in B) \tag{neq} \\ A \subseteq B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B \tag{subset-eq} \\ A \subsetneq B & \leftrightarrow & A \subseteq B \wedge A \neq B \tag{subset-neq} \end{align}

Proof.

$$\begin{matrix} A \subseteq B \wedge B \subseteq A & \rightarrow & \forall x, x \in A \leftrightarrow x \in B & \textrm{by (subset-eq) and intuition} \\ & \leftrightarrow & A = B & \textrm{by (eq)} \\ \\ A \subsetneq B & \leftrightarrow & A \subseteq B \wedge A \neq B & \textrm{by (subset-neq)} \\ & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \\ & & \wedge & \\ & & \exists x, (x \in A \wedge x \not\in B) \vee (x \in B \wedge x \not\in A) & \textrm{by (subset-eq) and (neq)} \\ & \rightarrow & \forall x, x \in A \rightarrow x \in B \wedge \exists x, x \in B \wedge x \not\in A & \textrm{by intuition} \\ \\\\ B \subsetneq C & \rightarrow & \forall x, x \in B \rightarrow x \in C & \\ & & \wedge & \\ & & \exists x, x \in C \wedge x \not\in B & \textrm{by similar argument} \\ \\\\ A \subsetneq B \wedge B \subsetneq C & \rightarrow & \forall x, x \in A \rightarrow x \in C & \\ & & \wedge & \\ & & \exists x, x \in C \wedge x \not\in A & \textrm{by intuition} \\ & \rightarrow & A \subseteq C \wedge C \neq A & \textrm{by (subset-eq) and (neq)} \\ & \rightarrow & A \subsetneq C & \textrm{by (subset-neq)} \end{matrix}$$

Qed.

Show that, for any two sets $A, B$, $$A \subseteq B \leftrightarrow A \cup B = B \leftrightarrow A \cap B = A$$

Hypothesis:

\begin{align} A \subseteq B & = & \forall x &, x \in A \rightarrow x \in B \tag{subset-eq} \\ A \cup B & = & \forall x &, x \in A \vee x \in B \tag{union} \\ A \cap B & = & \forall x &, x \in A \wedge x \in B \tag{intersect} \end{align}

Proof.

$$\begin{matrix} A \cup B = B & \leftrightarrow & \forall x, x \in A \cup B \leftrightarrow x \in A \vee x \in B = B & \textrm{by (union)} \\ & \leftrightarrow & \forall x, x \in A \vee x \in B \leftrightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & A \subseteq B & \textrm{by (subset-eq)} \\ \\\\ A \cap B = A & \leftrightarrow & \forall x, x \in A \wedge x \in B \leftrightarrow x \in A & \textrm{by (intersect) and intuition} \\ & \leftrightarrow & \forall x \in A \rightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & A \subseteq B & \textrm{by (subset-eq)} \end{matrix}$$

Qed.

(3.3.4) Show that injective corresponds to left-cancelable, and dually, surjective corresponds to right-cancelable, in function composition.

Definitions:

\begin{align} \forall x, \tilde{x} \in X, f(x) = f(\tilde{x}) \rightarrow x = \tilde{x} \tag{injective} \\ \forall y \in Y, \exists x \in X, f(x) = y \tag{surjective} \\ \end{align}

Parameters:

\begin{align} f, \tilde{f} : X \rightarrow Y \tag{xy-funcs} \\ g, \tilde{g} : Y \rightarrow Z \tag{yz-funcs} \end{align}

Goal:

\begin{align} && g \circ f = g \circ \tilde{f} & \tag{G1.1} \\ && \wedge \\ && g \textrm{ is injective} & \tag{G1.2} \\ & \leftrightarrow & f = \tilde{f} & \tag{G1.3} \\ \\\\ && g \circ f = \tilde{g} \circ f & \tag{G2.1} \\ && \wedge & \\ && f \textrm{ is surjective} & \tag{G2.2} \\ & \leftrightarrow & g = \tilde{g} & \tag{G2.3} \end{align}

Proof.

$$\begin{matrix} f(x) & = & y & \textrm{(H1.1)} \\ \tilde{f}(x) & = & \tilde{y} & \textrm{(H1.2)} \\ \\ g(y) = g(\tilde{y}) \wedge g \textrm{ is injective} & \leftrightarrow & y = \tilde{y} & \textrm{by (G1.2) and (injective)} \\ & \leftrightarrow & \forall x, f(x) = \tilde{f}(x) & \textrm{by (H1.1) and (H1.2)} \\ & \leftrightarrow & f = \tilde{f} & \textrm{obtained (G1.3)} \\ \\\\ g(y) & = & z & \textrm{(H2.1)} \\ \tilde{g}(y) & = & \tilde{z} & \textrm{(H2.2)} \\ \\ \forall x, (g \circ f)(x) = (\tilde{g} \circ f)(x) \wedge f \textrm{ is surjective} & \leftrightarrow & z = \tilde{z} & \textrm{by (G2.2) and (surjective)} \\ & \leftrightarrow & \forall y, g(y) = \tilde{g}(y) & \textrm{by (H2.1), and (H2.2)} \\ & \leftrightarrow & g = \tilde{g} & \textrm{obtained (G2.3)} \end{matrix}$$

Qed.

(3.3.5) Show that if $g \circ f$ is injective, then so is $f$. Dually, show that if $g \circ f$ is surjective, so is $g$.

Definitions:

\begin{align} \forall x, \tilde{x} \in X, f(x) = f(\tilde{x}) \rightarrow x = \tilde{x} \tag{injective} \\ \forall y \in Y, \exists x \in X, f(x) = y \tag{surjective} \end{align}

Parameters:

\begin{align} f : X \rightarrow Y \tag{f-func} \\ g : Y \rightarrow Z \tag{g-func} \end{align}

Goal:

\begin{align} g \circ f \textrm{ is injective} \rightarrow f \textrm{ is injective} \tag{G1} \\ g \circ f \textrm{ is surjective} \rightarrow g \textrm{ is surjective} \tag{G2} \end{align}

Proof.

$$\begin{matrix} \forall x, \tilde{x}, (g \circ f)(x) = (g \circ f)(\tilde{x}) & \rightarrow & x = \tilde{x} \wedge f(x) = f(\tilde{x}) & \textrm{by (injective) and definition of function} \\ & \leftrightarrow & f \textrm{ is injective} & \textrm{obtained (G1) by (injective)} \\ \\\\ \forall z, \exists x, z = (g \circ f)(x) & \rightarrow & \forall z, \exists y, z = g(y) & \textrm{by (surjective)} \\ & \leftrightarrow & g \textrm{ is surjective} & \textrm{obtained (G2) by (surjective)} \end{matrix}$$

Qed.

(3.4.1) Show that the universal specification axiom implies six simpler naïve set-theory axioms.

Hypothesis:

\begin{align} y \in \{x \mid P(x) \textrm{ is true}\} \leftrightarrow P(y) \textrm{ is true} \tag{H} \end{align}

Goal:

\begin{align} \forall x, x \not\in \emptyset \tag{G1} \\ \forall x, x \in \{a\} \leftrightarrow x = a \tag{G2} \\ \forall x, x \in \{a, b\} \leftrightarrow (x = a) \vee (x = b) \tag{G3} \\ x \in A \cup B \leftrightarrow x \in A \vee x \in B \tag{G4} \\ y \in \{x \in A \mid Q(x) \textrm{ is true}\} \leftrightarrow y \in A \wedge Q(y) \textrm{ is true} \tag{G5} \\ z \in \{y \mid Q(x, y) \textrm{ is true for some } x \in A\} \leftrightarrow Q(x, z) \textrm{ is true for some } x \in A \tag{G6} \end{align}

Proof.

To prove each of $\textrm{(G1) - (G6)}$, we simply find a suitable $P(x)$ to use in $\textrm{(H)}$:

$$\begin{matrix} P(x) = \textrm{ false} & \textrm{obtained (G1)} \\ P(x) = (x = a) & \textrm{obtained (G2)} \\ P(x) = (x = a) \vee (x = b) & \textrm{obtained (G3)} \\ P(x) = (x \in A) \vee (x \in B) & \textrm{obtained (G4)} \\ P(x) = Q(x) \wedge x \in A & \textrm{obtained (G5)} \\ P(x) = \exists y. x \in A \wedge P(x, y) \textrm{ is true} & \textrm{obtained (G6)} \end{matrix}$$

Qed.

† Thanks to [Chaitanya Leena Subramanium](https://sites.google.com/view/chaitanyals) for suggesting the exercises.

‡ Thanks to [Hugo Herbelin](http://pauillac.inria.fr/~herbelin/) for patiently going through many proofs and pointing out the errors.