← MA0 1 · Introduction to University Mathematics (Proofs)

Lesson 3

Naive Sets

Taught 13 Aug 2026

Sets

In the last chapter, we introduced predicates, quantifiers, and (most importantly) sets, attempting to characterise our mathematical discourse around them as well-defined; although we now possess the necessary tools to work with them directly, we will still set out a formal framework: a system of axioms for sets, just as we established for logic in Chapter 1. The result will be a somewhat overcomplete collection of axioms (a style not typically used when teaching set theory); some of these axioms can be used to deduce others.

Axioms

The previous definition of the set as nothing more than a collection of objects, although circular as collection is merely a set under a different name, is useful and intuitive enough that to form a collection of object is to abstract from the intrinsic nature of the items themselves.

The logicians have in any case turned this into a method by asking where an object sits rather than what it is. A set, in this picture, is a “primary” box holding other “secondary” boxes, its elements, which may contain further boxes in their turn, and so on as far down as one cares to follow; the composition of the box never matters, only the arrangement of which box lies within which, so that two boxes with the same contents are the same box. The picture asks two things of us:

Axiom 3.1 (Existence).

There exists a set with no elements, $\exists X\,\forall x\,(x \notin X)$ : called the empty or null set, written as $\{\}$ or $\emptyset$ .

Axiom 3.2 (Sets are objects).

If $A$ is a set, then $A$ is also an object. In particular, a box $A$ is itself an object and an object may go inside a box $B$ , and therefore it is meaningful to ask whether $A$ is also an element of $B$ .

Remark.

Georg Cantor built set theory on that move somewhere between 1870 and 1890, taking the totality of objects sharing a given property to be one new object. The subject so founded divides into two: a first-order study of the sets themselves, and a higher-order study that turns upon the first to ask how far such knowledge can reach, where it shades into metamathematics, (we wont study this far). The creation itself irritated his contemporaries, for such an object might be infinite, and to enclose an infinity within a single box was more than most would grant.

Using our picture, we summarise the two relations used to build up set theory. The first, introduced last chapter, is the membership relation $x \in X$ : if $x$ is an object and $X$ is a set, then $x \in X$ is either true or false (it is well defined, which we come to in a second); note that if $X$ is not a set then $x \in X$ does not make sense, like saying $\pi \in 3$ . The second is the equality relation $x = y$ : $x$ and $y$ name the same object, and its negation is written $\lnot(x=y)$ or $x \neq y$ . The equality relation obeys the three laws one expects: reflexivity, $x = x$ ; symmetry, if $x = y$ then $y = x$ ; and transitivity, if $x = y$ and $y = z$ then $x = z$ . The two relations, $\in$ and $=$ , obey axioms we will state as we need them; when the objects named are sets, the axiom of extension below tells us how to recognise that sameness.

Remark (Substitution).

Given any two objects $x$ and $y$ with $x = y$ , the statements $P(x)$ and $P(y)$ are equivalent for every property $P$ depending on $x$ . This is customarily taken as the axiom of substitution, but we are not assuming anything new: a predicate had its truth value fixed by the objects assigned to its variables rather than by the terms naming them, and $x = y$ says those two terms name one object, so $P(x)$ and $P(y)$ are the same assignment twice over.

Axiom 3.3 (Extensionality).

If two sets $A$ and $B$ , have the exact same elements then they are equal, $\forall A\forall B(\forall x(x \in A \iff x \in B) \implies A=B).$

From the axiom we know that sets are unordered, as the biconditional shows, and that repetition does not count, as the box picture makes plain. There is no point in dropping two secondary boxes $A$ and $B$ into $X$ when, opened all the way down, they hold the same contents; they are not distinct objects, however distinct they may look.

Example 3.4.

The sets $\{2, 2, 3, 4, \pi, \emptyset\}$ and $\{4, \pi, \emptyset, 2, 3\}$ are equal.

From these axioms we prove that the equality extensionality gives us for sets obeys them too.

Theorem 3.5 (Equality of sets is an equivalence relation).

Let $A$ , $B$ and $C$ be sets. Then $A = A$ ; if $A = B$ then $B = A$ ; and if $A = B$ and $B = C$ then $A = C$ .

Since $A = B$ is the statement $\forall x\,((x \in A) \iff (x \in B))$ , we prove it just as proving universal claims taught us to prove any universally quantified biconditional: take an arbitrary $x$ , and show that $x \in A$ and $x \in B$ stand or fall together.

Discussion.

Every one of the three claims has the same form once extensionality is applied: We first note that the biconditional splits into its two constituents, $(x \in A \implies x \in B) \land (x \in B \implies x \in A)$ , so each law fixes an arbitrary object $x$ , proves two implications about its membership. For reflexivity, $A = A$ , or $(x \in A \implies x \in A) \land (x \in A \implies x \in A)$ ; there is no hypothesis to argue from, so we read the implication through the defining equivalence of the conditional as $\neg(x \in A) \lor (x \in A)$ , which Complement makes $\top$ , and a conjunction of two such is $\top$ again. For symmetry we assume $A = B$ , or, $(x \in A \implies x \in B) \land (x \in B \implies x \in A)$ ; by Commutativity of $\land$ , gives us $(x \in B \implies x \in A) \land (x \in A \implies x \in B)$ which is $B=A$ . For transitivity we assume $A = B$ and $B = C$ , which give four implications between three memberships: $x \in A \implies x \in C$ is the chain of $x \in A \implies x \in B$ with $x \in B \implies x \in C$ by hypothetical syllogism, and $x \in C \implies x \in A$ is the chain of the other two the same way.

Proof (element style).

Let $x$ be an object.

For reflexivity, we must show that $x$ lies in $A$ exactly when it lies in $A$ . If $x \in A$ then $x \in A$ , and if $x \notin A$ then $x \notin A$ , so the two memberships stand or fall together whichever way $x$ falls. As $x$ was arbitrary, Axiom 3.3 gives $A = A$ .

For symmetry, suppose $A = B$ . Then $x \in A \iff x \in B$ by substitution. If $x \in B$ then that biconditional puts $x$ in $A$ , and if $x \in A$ it puts $x$ in $B$ , so $x \in B \iff x \in A$ . As $x$ was arbitrary, Axiom 3.3 gives $B = A$ .

For transitivity, suppose $A = B$ and $B = C$ . Then $x \in A \iff x \in B$ and $x \in B \iff x \in C$ by substitution. If $x \in A$ , the first carries it into $B$ and the second into $C$ ; if $x \in C$ , the second carries it back into $B$ and the first into $A$ . So $x \in A \iff x \in C$ , and as $x$ was arbitrary, Axiom 3.3 gives $A = C$ .

The axiom of extensionality also tells us that the empty set is unique.

Proposition 3.6 (Uniqueness of the empty set).

There is exactly one set with no elements.

Discussion.

By Axiom 3.1 , we know there is at least one set with no elements, so uniqueness is the claim that any two such sets are equal. Suppose $\emptyset'$ is a different set that doesnt have any elements. By definition $\emptyset$ must equal $\emptyset'$ , which by Axiom 3.3 , $\emptyset = \emptyset'$ is the statement $\forall x\,(x \in \emptyset \iff x \in \emptyset')$ , for an arbitrary object $x$ . Neither set $\emptyset$ , and $\emptyset'$ has elements, so both of its sides are $\bot$ , and $\bot \iff \bot$ is $\top$ by biconditional.

Proof.

Let $\emptyset$ and $\emptyset'$ both be sets with no elements, and let $x$ be an object. Since $\emptyset$ has no elements, $x \notin \emptyset$ , and since $\emptyset'$ has no elements, $x \notin \emptyset'$ ; both $x \in \emptyset$ and $x \in \emptyset'$ are therefore $\bot$ . By the biconditional, $\bot \iff \bot$ is $\top$ , so $x \in \emptyset \iff x \in \emptyset'$ . As $x$ was arbitrary, Axiom 3.3 gives $\emptyset = \emptyset'$ . Any two sets with no elements are equal, so there is only one, and we are entitled to speak of the empty set.

If a set is not equal to the empty set we call it non-empty. The following is a small statement, but one we will lean on often.

Proposition 3.7 (Single choice).

Let $A$ be a non-empty set. Then there exists an object $x$ such that $x \in A$ .

Discussion.

The statement is existential, and proving existential claims asks for a witness, which the hypothesis $A \neq \emptyset$ does not name. We prove it by contradiction: denying the conclusion makes $x \in A$ false for every object $x$ , and $x \in \emptyset$ is false by Axiom 3.1 , so $x \in A \iff x \in \emptyset$ is $\top$ by the biconditional and Axiom 3.3 gives $A = \emptyset$ , against the hypothesis.

Proof.

Suppose, for contradiction, that no object $x$ satisfies $x \in A$ . Let $x$ be an object. Then $x \notin A$ , and by the axiom of existence $x \notin \emptyset$ . Both memberships are false, and as $x$ was arbitrary, $\emptyset = A$ (by Axiom 3.3 as $x \in A \iff x \in \emptyset$ is true), contradicting $A$ being non-empty, so some object $x$ satisfies $x \in A$ .

Remark.

Firstly The emptyset is not the same thing as the number 0. One is a set; and the other a number. Secondly Proposition 3.7 is what licenses the word “choose”: given a non-empty $A$ we may pick out an element of it and give that element a name, and it is the hypothesis $A \neq \emptyset$ that earns us the right to do so. Taking one element from each of finitely many non-empty sets $A_1, \ldots, A_n$ at once is a further step, and we will take it when we need it. Taking one from each of infinitely many is a different matter again: nothing we have assumed so far reaches that far, and it takes an axiom of its own, the axiom of choice, which we will keep running into.

Problem 3.1.

Let $A$ and $B$ be sets. Show that $A \neq B$ if and only if there is an object belonging to one of them and not to the other.

Set-Builder Notation

We go back to last chapter, where we combined sets with predicates. To describe a set by a defining characteristic, or by carving a condition into a larger set, we use set-builder notation; a set so described takes the form

S = \{x \mid P(x)\}

read ” $S$ is the set of all $x$ such that $P(x)$ is true”, with " $\mid$ " meaning such that (note that some people use " $:$ " over ”|”) and $P(x)$ a predicate.

This right now sounds like the well-defined set we spoke of earlier, but it isnt. As written the notation is unrestricted, and Russell’s paradox is what that costs us. Define

R = \{x \mid x \notin x\}

We can ask a few questions, like what the elements of $R$ are. Any of the sets we have discussed so far would be one: the empty set contains no elements, so it certainly does not have itself as an element, and $\emptyset \in R$ . But what about $R$ itself?

Suppose $R \in R$ . The defining property of $R$ tells us that each of its elements is a set which does not have itself as an element, so $R \notin R$ .
Suppose $R \notin R$ . Then $R$ is a set which does not have itself as an element, and that is the defining property, so $R \in R$ .

Each assumption gives us its own negation, so $R \in R \iff R \notin R$ . Nothing behaves this way, and the fault is not with $R$ but with the notation that produced it: we let the predicate range over everything at once.

Problem 3.2.

Is $\{x \mid x \neq x\}$ a paradoxical set? Say why or why not; (b) does it have any elements?

So currently written our set-builder notation isnt safe. The axiom below is what makes it safe, and it carves into a set we already have.

Axiom 3.8 (Comprehension).

For every set $A$ and every predicate $P(x)$ there exists a set whose elements are exactly the elements of $A$ for which $P(x)$ holds, $\forall A\,\exists B\,\forall x\,(x \in B \iff x \in A \land P(x))$ .

The predicate no longer ranges over everything; it ranges over the elements of a set we are holding already, so Russell’s $R$ is never formed. What we may write down instead is $\{x \in A \mid x \notin x\}$ , which is a perfectly ordinary set, and asking whether it belongs to itself gets an ordinary answer.

Proposition 3.9 (The carved set is unique).

Let $A$ be a set and $P(x)$ a predicate. There is exactly one set $B$ such that $x \in B$ if and only if $x \in A$ and $P(x)$ .

Discussion.

Axiom 3.8 supplies at least one such $B$ , so uniqueness is the claim that any two are equal. We prove this directly: We assume there is a second set $B'$ satisfying the same membership condition. By Axiom 3.3 , $B = B'$ is the statement $\forall x\,(x \in B \iff x \in B')$ , and the work is that one biconditional at an arbitrary object $x$ . Both sets carry the same membership criterion, so each side of it is equivalent to $x \in A \land P(x)$ , and the two sides are joined through that.

Proof.

Let $B$ and $B'$ both satisfy the criterion, and let $x$ be an object. Then $x \in B' \iff x \in A \land P(x)$ and $x \in A \land P(x) \iff x \in B$ , so $x \in B' \iff x \in B$ by the transitivity of equivalence. As $x$ was arbitrary, Axiom 3.3 gives $B = B'$ .

Since there is only one such set, we may name it.

Definition 3.10 (Set-builder notation).

Let $A$ be a set and $P(x)$ a predicate. The unique set $B$ such that $x \in B$ if and only if $x \in A$ and $P(x)$ is written $\{x \in A \mid P(x)\}$ .

The criterion settles membership one object at a time: given any object $x$ , whether $x \in \{x \in A \mid P(x)\}$ holds is decided by whether $x \in A$ and $P(x)$ do, and both of those have a truth value already.

Definition 3.11 (Well-defined set).

A set $X$ is well defined when $x \in X$ has a truth value for every object $x$ .

We note that every set Axiom 3.8 builds is well defined, since $P$ is a predicate and a predicate has a truth value once its variable is assigned.

Problem 3.3.

Let $A$ and $B$ be sets. Show that the set of objects lying in $A$ and not in $B$ exists.

We said at the outset that our collection of axioms would be somewhat overcomplete, and here is one instance of it: Axiom 3.1 asks for a set with no elements, but comprehension will produce one from any set at all.

Proposition 3.12 (Existence from comprehension).

Suppose some set exists. Then there is a set with no elements.

Discussion.

The hypothesis names a set but says nothing about its elements, so we can neither point at an object in it nor rule one out. What Axiom 3.8 lets us do is carve that set by any predicate we please, so we pick one no object can satisfy: $x \neq x$ fails for every object by the reflexivity of equality, and the set it carves out is then empty whatever we started from.

Proof.

Let $A$ be a set. By Axiom 3.8 , $B = \{x \in A \mid x \neq x\}$ is a set, and $x \in B \iff x \in A \land x \neq x$ for every object $x$ . Since $x = x$ for every object, $x \neq x$ is $\bot$ , and $x \notin B$ . As $x$ was arbitrary, $B$ has no elements.

The gain from restricting the notation is a set theory that does not fall over. What we give up is the set of everything.

Proposition 3.13 (No set of all sets).

There is no set $V$ such that every set is an element of $V$ , that is, $\neg\exists V\,\forall X\,(X \in V)$ , with $X$ ranging over sets.

Discussion.

The claim is a negative existence statement, so we prove it by contradiction: we assume such a $V$ exists and use it to build a set that cannot exist. Axiom 3.8 applied to $V$ and the predicate ” $x$ is not an element of itself” produces $R = \{x \in V \mid x \notin x\}$ , which is where Russell’s argument runs again, this time inside the axiom rather than outside it. The question is whether $R \in R$ , and the membership criterion is a biconditional, $x \in R \iff x \in V \land x \notin x$ , so either answer forces the other.

Proof.

Suppose $V$ is a set containing every set. By Axiom 3.8 , $R = \{x \in V \mid x \notin x\}$ is a set, and since $V$ contains every set, $R \in V$ . If $R \in R$ , then by the membership criterion $R$ satisfies the defining predicate, so $R \notin R$ ; if $R \notin R$ , then $R \in V$ and $R \notin R$ both hold, which is the criterion, so $R \in R$ . Each alternative gives its own negation, so no such $V$ exists.

Pairs

Were these the only axioms we had, set theory would be a paper thin subject: Axiom 3.1 gives us the empty set, and Axiom 3.8 only ever carves into a set we are already holding, so every set we could name would be empty. The axioms below build.

Axiom 3.14 (Pairing).

For any two objects there is a set containing exactly those two, $\forall x\,\forall y\,\exists z\,\forall w\,(w \in z \iff (w = x \lor w = y))$ .

Definition 3.15 (Pair and singleton).

Let $x$ and $y$ be objects. The set given by pairing them is written $\{x, y\}$ , and we write $\{x\}$ for $\{x, x\}$ , the singleton of $x$ .

Remark.

The axiom asserts that such a set exists; that there is only one comes from Axiom 3.3 , by the argument of Proposition 3.9 . Two sets answering to the same membership criterion agree on every object, so they are equal; the same holds for every set we name from here on.

Since $\{x\}$ is an abbreviation rather than a further axiom, no separate axiom for singletons is needed: pairing an object with itself produces one.

Remark.

From here on there are two natural styles for writing such a proof. The first chases the element through in prose, spelling out what each membership means as it goes; the second works directly on the predicates, transforming " $x \in A$ " into " $x \in B$ " by the laws tabulated in the first chapter. Both are correct, and tastes differ; I prefer the logical style, but I will give both throughout for completeness, and you should be able to read each.

Proposition 3.16 (Pairs are unordered and absorb repetition).

Let $x$ and $y$ be objects. Then $\{x, y\} = \{y, x\}$ , and $w \in \{x\}$ if and only if $w = x$ , for every object $w$ .

Discussion.

The first claim is an equality of sets, so by Axiom 3.3 it is a biconditional at an arbitrary object $w$ , and the membership criterion of Axiom 3.14 rewrites each side as a disjunction: $w = x \lor w = y$ on the one side and $w = y \lor w = x$ on the other, which the axiom of Commutativity exchanges. The second claim is not an equality of sets, since $\{x\}$ is by Definition 3.15 another name for $\{x, x\}$ ; what has to be shown is that the pair criterion collapses, $w = x \lor w = x$ reducing to $w = x$ by Idempotence, so that the singleton holds the one object and nothing else.

Proof (element style).

Let $w$ be an object and suppose $w \in \{x, y\}$ . By Axiom 3.14 , $w = x$ or $w = y$ . In the first case $w$ is the second of the two objects paired to form $\{y, x\}$ , and in the second case it is the first, so $w \in \{y, x\}$ either way. Interchanging $x$ and $y$ throughout carries an element of $\{y, x\}$ back to $\{x, y\}$ . As $w$ was arbitrary, Axiom 3.3 gives $\{x, y\} = \{y, x\}$ . For the singleton, $\{x\}$ is $\{x, x\}$ . If $w \in \{x\}$ , then by Axiom 3.14 $w = x$ or $w = x$ , and both alternatives say the same thing, so $w = x$ . Conversely, if $w = x$ then the first alternative holds, so $w \in \{x, x\}$ , which is $w \in \{x\}$ .

Proof (logical style).

Let $w$ be an object.

\begin{aligned} w \in \{x, y\} &\equiv (w = x \lor w = y) && \text{by Pairing} \\ &\equiv (w = y \lor w = x) && \text{by Commutativity} \\ &\equiv w \in \{y, x\} && \text{by Pairing} \end{aligned}

As $w$ was arbitrary, Axiom 3.3 gives $\{x, y\} = \{y, x\}$ . For the singleton:

\begin{aligned} w \in \{x\} &\equiv w \in \{x, x\} && \text{by the singleton notation} \\ &\equiv (w = x \lor w = x) && \text{by Pairing} \\ &\equiv w = x && \text{by Idempotence} \end{aligned}

Example 3.17.

The empty set is a set, hence an object by Axiom 3.2 , so pairing it with itself gives the singleton $\{\emptyset\}$ . That in turn is an object, so we may form $\{\{\emptyset\}\}$ , and pairing the first two gives $\{\emptyset, \{\emptyset\}\}$ .

Problem 3.4.

Show that $\emptyset$ , $\{\emptyset\}$ , $\{\{\emptyset\}\}$ and $\{\emptyset, \{\emptyset\}\}$ are four different sets.

Every set we can build so far holds at most two elements; to grow them we take a set whose members are themselves sets and pool everything they contain.

Axiom 3.18 (Union).

Given any set of sets, there is a set containing precisely those objects which are members of some set in the collection, $\forall x\,\exists y\,\forall z\,(z \in y \iff \exists w\,(z \in w \land w \in x))$ .

Definition 3.19 (Union of a system of sets).

Let $S$ be a set. The unique set $U$ such that $x \in U$ if and only if $x \in A$ for some $A \in S$ is written $\bigcup S$ .

Definition 3.20 (Union of two sets).

Let $A$ and $B$ be sets. Then $A \cup B$ denotes the set $\bigcup \{A, B\}$ .

Two axioms are at work in that second definition: pairing gathers $A$ and $B$ into one collection, and union pools what they hold. Membership in the result reads as a disjunction.

Proposition 3.21 (Membership in a union).

Let $A$ and $B$ be sets. For every object $x$ , $x \in A \cup B \iff (x \in A \lor x \in B)$ .

Discussion.

$A \cup B$ is $\bigcup \{A, B\}$ , so Axiom 3.18 reads its membership as $\exists w\,(x \in w \land w \in \{A, B\})$ , an existential claim about which member of the collection holds $x$ . The collection has only two members, since Axiom 3.14 gives $w \in \{A, B\} \iff (w = A \lor w = B)$ , so the witness $w$ can only be $A$ or $B$ and the existential claim collapses into the disjunction of those two cases.

Proof (element style).

Let $x$ be an object and suppose $x \in A \cup B$ , which is to say $x \in \bigcup \{A, B\}$ . By Axiom 3.18 some set $w$ has $x \in w$ and $w \in \{A, B\}$ , and by Axiom 3.14 that $w$ is either $A$ or $B$ . In the first case $x \in A$ and in the second $x \in B$ , so $x \in A$ or $x \in B$ .

Conversely, suppose $x \in A$ or $x \in B$ . If $x \in A$ , take $w$ to be $A$ : then $x \in w$ , and $w \in \{A, B\}$ by Axiom 3.14 , so $w$ is a witness and $x \in \bigcup \{A, B\}$ . If instead $x \in B$ , take $w$ to be $B$ and argue the same way. Either way $x \in A \cup B$ .

Proof (logical style).

Let $x$ be an object.

\begin{aligned} x \in A \cup B &\equiv x \in \textstyle\bigcup \{A, B\} && \text{by the definition of } A \cup B \\ &\equiv \exists w\,(x \in w \land w \in \{A, B\}) && \text{by Union} \\ &\equiv \exists w\,\bigl(x \in w \land (w = A \lor w = B)\bigr) && \text{by Pairing} \\ &\equiv \exists w\,\bigl((x \in w \land w = A) \\ &\qquad\qquad {}\lor (x \in w \land w = B)\bigr) && \text{by Distributivity} \\ &\equiv \exists w\,(x \in w \land w = A) \\ &\qquad {}\lor \exists w\,(x \in w \land w = B) && \text{by }\exists\text{-distribution} \\ &\equiv (x \in A \lor x \in B) && \text{by substitution} \end{aligned}

The fifth step is the distribution of an existential over a disjunction from the last chapter, and the last discharges each witness by substitution, since a $w$ with $w = A$ may be replaced by $A$ throughout.

The “or” is the disjunction of the first chapter, inclusive as always, so an object lying in both sets lies in the union too.

Proposition 3.22 (Union is well defined).

Let $A$ , $A'$ and $B$ be sets with $A = A'$ . Then $A \cup B = A' \cup B$ .

Discussion.

An operation on sets should not depend on how we happened to name its arguments, and the criterion of Proposition 3.21 is what secures that here: membership in $A \cup B$ is decided by membership in $A$ and in $B$ , and $A = A'$ makes membership in $A$ and in $A'$ the same question. So the two unions meet the same criterion at every object, and Axiom 3.3 does the rest.

Proof (element style).

Let $x$ be an object and suppose $x \in A \cup B$ . By Proposition 3.21 , $x \in A$ or $x \in B$ . If $x \in A$ , then $x \in A'$ by substitution, since $A = A'$ ; if $x \in B$ , there is nothing to change. Either way $x \in A'$ or $x \in B$ , so $x \in A' \cup B$ by Proposition 3.21 .

For the converse, $A' = A$ by the symmetry of equality established in Theorem 3.5 , so the same argument run with $A'$ in place of $A$ carries an element of $A' \cup B$ into $A \cup B$ . As $x$ was arbitrary, Axiom 3.3 gives $A \cup B = A' \cup B$ .

Proof (logical style).

Let $x$ be an object.

\begin{aligned} x \in A \cup B &\equiv (x \in A \lor x \in B) && \text{by membership in a union} \\ &\equiv (x \in A' \lor x \in B) && \text{since } A = A' \\ &\equiv x \in A' \cup B && \text{by membership in a union} \end{aligned}

As $x$ was arbitrary, Axiom 3.3 gives $A \cup B = A' \cup B$ .

With membership in a union settled, the basic properties of the operation follow from the corresponding properties of $\lor$ .

Proposition 3.23 (Basic properties of unions).

Let $a$ and $b$ be objects and let $A$ , $B$ and $C$ be sets. Then

$\{a, b\} = \{a\} \cup \{b\}$ ;
$A \cup B = B \cup A$ ;
$(A \cup B) \cup C = A \cup (B \cup C)$ ;
$A \cup A = A \cup \emptyset = \emptyset \cup A = A$ .

Discussion.

Every claim is an equality of sets, so by Axiom 3.3 each is a biconditional at an arbitrary object $x$ , and Proposition 3.21 turns each side into a disjunction of memberships. What is left is a propositional identity in each case: Commutativity of $\lor$ for the second claim, Associativity for the third, and for the fourth, Idempotence for $A \cup A$ together with the axiom of Identity for the two involving $\emptyset$ , since $x \in \emptyset$ is $\bot$ by Axiom 3.1 . The first claim is the one that reaches back further: Axiom 3.14 gives $x = a \lor x = b$ on the left, and Proposition 3.16 reads each singleton on the right as a single equation, so the two sides meet at the same disjunction.

Proof (element style).

Let $x$ be an object.

For the first claim, suppose $x \in \{a, b\}$ . By Axiom 3.14 , $x = a$ or $x = b$ . In the first case $x \in \{a\}$ by Proposition 3.16 , and in the second $x \in \{b\}$ , so either way $x \in \{a\} \cup \{b\}$ by Proposition 3.21 . Conversely, if $x \in \{a\} \cup \{b\}$ then $x \in \{a\}$ or $x \in \{b\}$ , so $x = a$ or $x = b$ , and $x \in \{a, b\}$ .

For the second, suppose $x \in A \cup B$ . Then $x \in A$ or $x \in B$ , which is to say $x \in B$ or $x \in A$ , so $x \in B \cup A$ . The same argument with $A$ and $B$ interchanged gives the reverse.

For the third, suppose $x \in (A \cup B) \cup C$ . Then $x \in A \cup B$ or $x \in C$ . If $x \in C$ , then $x \in B \cup C$ , and so $x \in A \cup (B \cup C)$ . If instead $x \in A \cup B$ , then $x \in A$ or $x \in B$ ; in the first case $x \in A \cup (B \cup C)$ at once, and in the second $x \in B \cup C$ and hence $x \in A \cup (B \cup C)$ . So every element of $(A \cup B) \cup C$ lies in $A \cup (B \cup C)$ , and a similar argument gives the reverse.

For the fourth, $x \in A \cup A$ says $x \in A$ or $x \in A$ , which says $x \in A$ . And $x \in A \cup \emptyset$ says $x \in A$ or $x \in \emptyset$ , where the second alternative is impossible by Axiom 3.1 , so it says $x \in A$ ; the same holds for $\emptyset \cup A$ .

In each case $x$ was arbitrary, so Axiom 3.3 gives the four equalities.

Proof (logical style).

Let $x$ be an object, and write $p$ , $q$ , $r$ for the propositions $x \in A$ , $x \in B$ , $x \in C$ .

\begin{aligned} x \in \{a, b\} &\equiv (x = a \lor x = b) && \text{by Pairing} \\ &\equiv (x \in \{a\} \lor x \in \{b\}) && \text{by the singleton criterion} \\ &\equiv x \in \{a\} \cup \{b\} && \text{by membership in a union} \end{aligned}

\begin{aligned} x \in A \cup B &\equiv p \lor q \equiv q \lor p \equiv x \in B \cup A && \text{by Commutativity} \\ x \in (A \cup B) \cup C &\equiv (p \lor q) \lor r \\ &\equiv p \lor (q \lor r) \equiv x \in A \cup (B \cup C) && \text{by Associativity} \\ x \in A \cup A &\equiv p \lor p \equiv x \in A && \text{by Idempotence} \\ x \in A \cup \emptyset &\equiv p \lor \bot \equiv x \in A && \text{by Identity} \end{aligned}

We note that $\emptyset \cup A$ goes the same way after Commutativity. In each case $x$ was arbitrary, so Axiom 3.3 gives the equalities.

Because of associativity, we do not need to use the brackets: $A \cup B \cup C$ names one set regardless of how we group it ( $A \cup (B \cup C)$ or $(A \cup B) \cup C$ , both mean the same thing), and likewise for $A \cup B \cup C \cup D$ and longer strings.

Definition 3.24 (Triples and longer).

Let $a$ , $b$ , $c$ be objects. We write $\{a, b, c\}$ for $\{a\} \cup \{b\} \cup \{c\}$ , and $\{a, b, c, d\}$ for $\{a\} \cup \{b\} \cup \{c\} \cup \{d\}$ , and so on for any string of objects written out in full.

Example 3.25.

The set $\{1, 2\} \cup \{2, 3\}$ holds those objects lying in $\{1,2\}$ , or in $\{2,3\}$ , or in both, which are $1$ , $2$ and $3$ . So $\{1, 2\} \cup \{2, 3\} = \{1, 2, 3\}$ .

The phrase “and so on” is doing work we cannot yet justify. Writing a set of $n$ objects for an unspecified $n$ means iterating the construction $n$ times, and we have not said what iterating a construction a given number of times amounts to; a set of infinitely many objects is further out of reach still. Later axioms will build sets that large.

Problem 3.5.

Let $A$ be a set. Show that $\bigcup \{A\} = A$ .

Subset

Comparing sets, we can see that some sit inside others, and we say the smaller one is a subset of the bigger. We write $\subset$ for this throughout, whether or not the two sets happen to be equal.

Definition 3.26 (Subset).

Let $A$ and $S$ be sets. We say $A$ is a subset of $S$ , written $A \subset S$ , if every element of $A$ is an element of $S$ . If moreover $A \neq S$ , we call $A$ a proper subset of $S$ and write $A \subsetneq S$ .

In logical language this is a universally quantified implication between predicates,

A \subset S \quad\text{means}\quad \forall x\,\bigl((x \in A) \implies (x \in S)\bigr),

and this reading will drive every subset proof we write: to prove $A \subset S$ we take an arbitrary $x$ , assume $x \in A$ , and reach $x \in S$ .

Example 3.27.

The empty set is a subset of every set $S$ . The implication $(x \in \emptyset) \implies (x \in S)$ has a hypothesis no object can satisfy, and an implication with a false hypothesis holds automatically; a promise never invoked is never broken. So $\emptyset \subset S$ , vacuously.

The definition uses nothing but $\in$ and $=$ , and both obey substitution, so the subset relation does too: if $A \subset B$ and $A = A'$ , then $A' \subset B$ .

Proposition 3.28 (Subsets are transitive).

Let $A$ , $B$ and $C$ be sets. If $A \subset B$ and $B \subset C$ , then $A \subset C$ .

Discussion.

The conclusion $A \subset C$ is itself a universally quantified implication, so we assume $x \in A$ for an arbitrary object $x$ and must reach $x \in C$ . The definition of subset is the only tool needed: $A \subset B$ trades membership in $A$ for membership in $B$ , and $B \subset C$ trades membership in $B$ for membership in $C$ , so the element walks through $B$ .

Proof (element style).

Let $x \in A$ . By the definition of subset, $A \subset B$ gives $x \in B$ , and $B \subset C$ gives $x \in C$ . As $x$ was arbitrary, $A \subset C$ .

Proof (logical style).

For any object $x$ ,

\begin{aligned} x \in A &\implies x \in B && \text{since } A \subset B \\ &\implies x \in C && \text{since } B \subset C, \end{aligned}

so $(x \in A) \implies (x \in C)$ holds for every $x$ , which is $A \subset C$ .

Mutual inclusion is the other way of saying two sets are equal, which is what we should expect: the obvious way to define equality of sets is to say they contain exactly the same elements, and that is two implications rather than one.

Proposition 3.29 (Mutual inclusion is equality).

Let $A$ and $B$ be sets. If $A \subset B$ and $B \subset A$ , then $A = B$ .

Discussion.

By Axiom 3.3 the conclusion is a biconditional at an arbitrary object $x$ , and by the defining equivalence of the biconditional that biconditional is the conjunction of two implications. Those two implications are exactly what the two inclusions say, so the hypotheses deliver the conclusion once we have unfolded both sides into their logical form.

Proof.

Let $x$ be an object. By the definition of subset, $A \subset B$ gives $x \in A \implies x \in B$ , and $B \subset A$ gives $x \in B \implies x \in A$ . The two together say that $x$ lies in $A$ exactly when it lies in $B$ , so $x \in A \iff x \in B$ . As $x$ was arbitrary, Axiom 3.3 gives $A = B$ .

Proposition 3.30 (Proper subsets are transitive).

Let $A$ , $B$ and $C$ be sets. If $A \subsetneq B$ and $B \subsetneq C$ , then $A \subsetneq C$ .

Discussion.

A proper inclusion is two claims, so the conclusion is two claims. The inclusion $A \subset C$ is Proposition 3.28 applied to the two inclusions we are given, which leaves $A \neq C$ . For that we need an object separating them, and $B \subsetneq C$ supplies one: were every element of $C$ in $B$ we would have $C \subset B$ , and with $B \subset C$ that makes $B = C$ by Proposition 3.29 , against $B \neq C$ . That object lies in $C$ but not in $B$ , so it cannot lie in $A$ either.

Proof.

From $A \subset B$ and $B \subset C$ we get $A \subset C$ by Proposition 3.28 , so it remains to show $A \neq C$ . Since $B \neq C$ , some object $c$ lies in $C$ but not in $B$ : otherwise every element of $C$ would be an element of $B$ , giving $C \subset B$ , and with $B \subset C$ that would make $B = C$ by Proposition 3.29 . Now suppose $A = C$ . Then $c \in A$ by substitution, and $A \subset B$ gives $c \in B$ , contradicting $c \notin B$ . So $A \neq C$ , and with $A \subset C$ this is $A \subsetneq C$ .

Problem 3.6.

Is $S \subset S$ for every set $S$ ?

Problem 3.7.

Let $S = \{1, 2\}$ . Which of $1 \in S$ , $\{1\} \in S$ and $\{1\} \subset S$ are true?

More Set Operations

Swapping the “or” for an “and” gives the intersection, whose members must belong to both sets at once.

Definition 3.31 (Intersection).

Let $S$ and $T$ be sets. The intersection $S \cap T$ is the set $\{x \in S \mid x \in T\}$ , so that for every object $x$ ,

(x \in S \cap T) \equiv (x \in S) \land (x \in T).

The intersection needs no new axiom: Axiom 3.8 carves it out of $S$ , a set we are already holding. And since it is defined from $\in$ and $\land$ alone, both of which obey substitution, so does the intersection. The same remark applies to the definitions that follow, and we will not mention it again.

Proposition 3.32 (Inclusions for union and intersection).

Let $S$ and $T$ be sets. Then $S \cap T \subset S$ and $S \cap T \subset T$ , while $S \subset S \cup T$ and $T \subset S \cup T$ .

Discussion.

Each of the four is a universally quantified implication, so each takes an arbitrary $x$ , assumes the left membership and reaches the right. The two for the intersection unfold into a conjunction on the left, and Simplification extracts either conjunct. The two for the union unfold into a disjunction on the right, and Addition weakens a known truth to a disjunction.

Proof.

Let $x$ be an object. If $x \in S \cap T$ , then $x \in S$ and $x \in T$ ; Simplification gives $x \in S$ from that conjunction, and equally $x \in T$ . As $x$ was arbitrary, $S \cap T \subset S$ and $S \cap T \subset T$ .

If instead $x \in S$ , then Addition gives $x \in S$ or $x \in T$ , which is $x \in S \cup T$ by Proposition 3.21 . As $x$ was arbitrary, $S \subset S \cup T$ , and the argument for $T$ is the same.

Definition 3.33 (Disjoint).

Two sets $A$ and $B$ are disjoint if $A \cap B = \emptyset$ .

Remark.

Being disjoint is not the same as being distinct. The sets $\{1, 2, 3\}$ and $\{2, 3, 4\}$ are distinct, since each holds an element the other does not, but they are not disjoint, since their intersection holds $2$ and $3$ . Meanwhile $\emptyset$ and $\emptyset$ are disjoint but not distinct.

Problem 3.8.

Let $S$ be a set. What is $S \cap \emptyset$ ?

Theorem 3.34 (Characterising the empty set).

Let $L$ be a set. The following are equivalent.

$L \subset M$ for every set $M$ ;
$M \cap L = L$ for every set $M$ ;
$L$ has no elements;
$M \cup L = M$ for every set $M$ .

Discussion.

Four statements would ordinarily need twelve implications, but a loop is enough: we prove the chain $1 \implies 2 \implies 3 \implies 4 \implies 1$ , and every statement then reaches every other by going round. Step $1 \implies 2$ is an equality of sets, so it is two inclusions, one of which we already have from Proposition 3.32 . Step $2 \implies 3$ has no object to point at, so it goes by contradiction, and the case $M = \emptyset$ is what collapses it. Step $3 \implies 4$ is again two inclusions, and the work is splitting the “or” in $x \in M \cup L$ , where the second alternative is ruled out by the hypothesis. Step $4 \implies 1$ is a single inclusion, read off Proposition 3.32 and the hypothesis.

Proof.

$1 \implies 2$ . Assume $L \subset M$ . We have $M \cap L \subset L$ by Proposition 3.32 . For the reverse inclusion take $x \in L$ ; then $x \in M$ since $L \subset M$ , so $x \in M$ and $x \in L$ , which is $x \in M \cap L$ . Hence $L \subset M \cap L$ , and Proposition 3.29 gives $M \cap L = L$ .

$2 \implies 3$ . Suppose, to the contrary, that $L$ has an element $x$ . Taking $M = \emptyset$ in the second statement gives $\emptyset \cap L = L$ . But nothing belongs to $\emptyset \cap L$ , since anything in it would lie in $\emptyset$ and Axiom 3.1 forbids that, so $\emptyset \cap L$ has no elements and $L$ has none either. This contradicts $x \in L$ .

$3 \implies 4$ . Assume $L$ has no elements. We have $M \subset M \cup L$ by Proposition 3.32 . For the reverse inclusion take $x \in M \cup L$ ; by Proposition 3.21 either $x \in M$ or $x \in L$ , and the second is impossible, so $x \in M$ . Hence $M \cup L \subset M$ , and Proposition 3.29 gives $M \cup L = M$ .

$4 \implies 1$ . Let $M$ be a set. We have $L \subset M \cup L$ by Proposition 3.32 , and $M \cup L = M$ by the fourth statement, so $L \subset M$ by substitution.

Complements of Sets

If $A \subset S$ , the complement of $A$ in $S$ is the set of all elements of $S$ that are not in $A$ .

Definition 3.35 (Complement).

Let $A \subset S$ . The complement of $A$ in $S$ is the set

\overline{A} \;\defeq\; \{x \in S \mid x \notin A\},

so that for $x$ ranging over $S$ , $(x \in \overline{A}) \equiv \neg(x \in A)$ .

Other texts write $A^{c}$ , but we will stick with $\overline{A}$ . Notice that a complement means nothing until the ambient set $S$ is understood.

The complement removes one set from another only when the first lies inside the second. Dropping that assumption gives the difference of two arbitrary sets.

Definition 3.36 (Set difference).

For sets $A$ and $B$ , the difference $A \setminus B$ is the set of elements of $A$ that are not in $B$ ,

A \setminus B \;\defeq\; \{x \in A \mid x \notin B\},

with membership $(x \in A \setminus B) \equiv (x \in A) \land \neg(x \in B)$ . The complement $\overline{A}$ is the difference $S \setminus A$ in the case $A \subset S$ .

Example 3.37.

$\{1, 2, 3, 4\} \setminus \{2, 4, 6\} = \{1, 3\}$ . The set being removed need not sit inside the set it is removed from; the elements the two do not share are simply ignored.

Problem 3.9.

With complements taken in $S$ , what are $\overline{S}$ , $\overline{\emptyset}$ and $\overline{\overline{A}}$ ? Name the logic law behind the last one.

Complements breed negative statements like $x \notin A$ , and the standard tool for proving those is proof by contradiction: to show a statement true, assume its negation and derive a contradiction; the contradiction cannot stand, so the assumption was false and the statement we wanted holds.

Proposition 3.38 (Complements reverse inclusion).

Let $A, B \subset S$ . If $A \subset B$ , then $\overline{B} \subset \overline{A}$ .

Discussion.

The conclusion is a universally quantified implication, so we take $x \in \overline{B}$ and must reach $x \in \overline{A}$ . Both memberships are negative statements by the definition of the complement, so what has to be shown is $x \notin A$ from $x \notin B$ , and that is the contrapositive of the implication $A \subset B$ hands us. Elementwise the same step is a contradiction: assume $x \in A$ , push it through $A \subset B$ to $x \in B$ , and collide with $x \notin B$ .

Proof (element style).

Let $x \in \overline{B}$ , so $x \in S$ and $x \notin B$ . Suppose $x \in A$ . Then $A \subset B$ gives $x \in B$ , contradicting $x \notin B$ , so $x \notin A$ . Since $x \in S$ , this is $x \in \overline{A}$ . As $x$ was arbitrary, $\overline{B} \subset \overline{A}$ .

Proof (logical style).

For any $x$ in $S$ ,

\begin{aligned} x \in \overline{B} &\equiv \neg(x \in B) && \text{by the complement} \\ &\implies \neg(x \in A) && \text{by contraposition, since } A \subset B \\ &\equiv x \in \overline{A} && \text{by the complement} \end{aligned}

so $(x \in \overline{B}) \implies (x \in \overline{A})$ for every $x$ in $S$ , which is $\overline{B} \subset \overline{A}$ .

Problem 3.10.

Let $A \subset S$ , with complements taken in $S$ . Prove that $A \cap \overline{A} = \emptyset$ and $A \cup \overline{A} = S$ .

Remark (The dictionary).

By now a dictionary has emerged: complement is $\neg$ , intersection is $\land$ , union is $\lor$ , subset is $\implies$ , and equality is $\iff$ . Any equivalence built from $\neg$ , $\land$ and $\lor$ alone translates through it into an identity of sets, so the table of laws in the first chapter doubles as a table of set identities.

Before taking complements of combinations we should check they may be taken at all. If $S$ and $T$ are subsets of $X$ , then so are $S \cup T$ and $S \cap T$ : an element of $S \cup T$ lies in $S$ or in $T$ and so in $X$ either way, and $S \cap T \subset S \subset X$ by Proposition 3.32 and Proposition 3.28 . Complements of both are therefore defined in $X$ .

Feeding De Morgan’s laws through the dictionary produces their set-theoretic form: the complement bar breaks over $\cap$ and $\cup$ , swapping one for the other.

Theorem 3.39 (De Morgan's laws for sets).

Let $S$ and $T$ be subsets of an ambient set. Then

\overline{S \cup T} = \overline{S} \cap \overline{T} \qquad\text{and}\qquad \overline{S \cap T} = \overline{S} \cup \overline{T}.

Discussion.

We prove the first; the second is identical work with the roles exchanged. Equality of sets is two inclusions by Proposition 3.29 , and both read the same way through the dictionary. For $x$ in the ambient set, membership in $\overline{S \cup T}$ is the negation of the disjunction $(x \in S) \lor (x \in T)$ ; the disjunctive De Morgan law rewrites that negation as the conjunction $\neg(x \in S) \land \neg(x \in T)$ , which by the definitions of complement and intersection is membership in $\overline{S} \cap \overline{T}$ . Each inclusion is one half of this biconditional, and the logical proof writes the whole equivalence down at once.

Proof (element style).

For the first inclusion, assume $x \in \overline{S \cup T}$ , so $x \notin S \cup T$ by the definition of the complement: it is not true that $x \in S$ or $x \in T$ . By De Morgan’s laws this means $x \notin S$ and $x \notin T$ , that is, $x \in \overline{S}$ and $x \in \overline{T}$ . Belonging to both, $x$ belongs to their intersection, so $x \in \overline{S} \cap \overline{T}$ and $\overline{S \cup T} \subset \overline{S} \cap \overline{T}$ .

For the second inclusion, assume $x \in \overline{S} \cap \overline{T}$ , so $x \in \overline{S}$ and $x \in \overline{T}$ , meaning $x \notin S$ and $x \notin T$ . By De Morgan’s laws again, ” $x \in S$ or $x \in T$ ” is false, so $x \notin S \cup T$ by Proposition 3.21 , and hence $x \in \overline{S \cup T}$ . Thus $\overline{S} \cap \overline{T} \subset \overline{S \cup T}$ , and the two inclusions give the equality.

Proof (logical style).

For any $x$ in the ambient set,

\begin{aligned} x \in \overline{S \cup T} &\equiv \neg(x \in S \cup T) && \text{by the complement} \\ &\equiv \neg\bigl((x \in S) \lor (x \in T)\bigr) && \text{by the union} \\ &\equiv \neg(x \in S) \land \neg(x \in T) && \text{by De Morgan's laws} \\ &\equiv (x \in \overline{S}) \land (x \in \overline{T}) && \text{by the complement} \\ &\equiv x \in \overline{S} \cap \overline{T} && \text{by the intersection} \end{aligned}

The biconditional holds for every $x$ , so Axiom 3.3 gives $\overline{S \cup T} = \overline{S} \cap \overline{T}$ .

The set law is the logic law read through the dictionary, and the logical proof is barely more than the act of reading it.

The Distributive Laws

De Morgan’s laws show union and intersection entangled through the complement; they also interact directly, one applied to the output of the other. The pattern is distribution, as with numbers, though sets are more even-handed about it: multiplication distributes over addition but not the other way round, while here each operation distributes over the other.

Theorem 3.40 (Distributive laws for sets).

Let $S$ , $T$ and $R$ be sets. Then

S \cup (T \cap R) = (S \cup T) \cap (S \cup R) \qquad\text{and}\qquad S \cap (T \cup R) = (S \cap T) \cup (S \cap R).

Discussion.

We prove the first. It is an equality of sets, so two inclusions. For $S \cup (T \cap R) \subset (S \cup T) \cap (S \cup R)$ we assume $x \in S \cup (T \cap R)$ ; a union assumption is an “or”, so we split into the cases $x \in S$ and $x \in T \cap R$ , and in each we must put $x$ in both $S \cup T$ and $S \cup R$ . For the reverse inclusion we assume $x \in (S \cup T) \cap (S \cup R)$ , which hands us two “or” statements at once; the clean way through is to split on whether $x \in S$ , since if not, each “or” is forced to its other option. The logical proof needs only the axiom of Distributivity applied to the membership predicates.

Proof (element style).

For the first inclusion, assume $x \in S \cup (T \cap R)$ , so $x \in S$ or $x \in T \cap R$ . If $x \in S$ , then $x \in S \cup T$ and $x \in S \cup R$ , so $x$ lies in their intersection. If instead $x \in T \cap R$ , then $x \in T$ and $x \in R$ ; the first puts $x$ in $S \cup T$ , the second puts $x$ in $S \cup R$ , and again $x$ lies in the intersection. Either case gives $x \in (S \cup T) \cap (S \cup R)$ , so $S \cup (T \cap R) \subset (S \cup T) \cap (S \cup R)$ .

For the second inclusion, assume $x \in (S \cup T) \cap (S \cup R)$ , so $x \in S \cup T$ and $x \in S \cup R$ ; that is, $x \in S$ or $x \in T$ , and at the same time $x \in S$ or $x \in R$ . If $x \in S$ , then $x \in S \cup (T \cap R)$ and we are done. If $x \notin S$ , then the first “or” forces $x \in T$ and the second forces $x \in R$ , so $x \in T \cap R$ and again $x \in S \cup (T \cap R)$ . Either way $(S \cup T) \cap (S \cup R) \subset S \cup (T \cap R)$ , and with both inclusions the sets are equal.

Proof (logical style).

Let $x$ be an object and write $s$ , $t$ , $r$ for the propositions $x \in S$ , $x \in T$ , $x \in R$ .

\begin{aligned} x \in S \cup (T \cap R) &\equiv s \lor (t \land r) && \text{by the definitions} \\ &\equiv (s \lor t) \land (s \lor r) && \text{by Distributivity} \\ &\equiv (x \in S \cup T) \land (x \in S \cup R) && \text{by the union} \\ &\equiv x \in (S \cup T) \cap (S \cup R) && \text{by the intersection} \end{aligned}

By Axiom 3.3 we have the equality.

The comparison is a habit by now: the elementwise proof of the second inclusion needed a small idea, splitting on whether $x \in S$ , while the logical proof needed no ideas at all, only the table.

Theorem 3.41 (The algebra of intersection).

Let $A$ , $B$ and $C$ be sets. Then

$A \cap A = A$ ;
$A \cap B = B \cap A$ ;
$(A \cap B) \cap C = A \cap (B \cap C)$ ;
$A \cap (A \cup B) = A$ and $A \cup (A \cap B) = A$ ;
$A \subset B$ if and only if $A \cap B = A$ if and only if $A \cup B = B$ .

Discussion.

The union halves of the first three are Proposition 3.23 , and these are the same rows of the table read with $\land$ in place of $\lor$ : idempotence, commutativity and associativity are the logic laws of those names, and each is one chain of equivalences. The fourth mixes the two operations, and is absorption. The fifth is different in kind, since it is not an identity but a comparison: the equivalences $x \in A \cap B \iff x \in A$ and $x \in A \cup B \iff x \in B$ each say exactly that $x \in A$ implies $x \in B$ , so we check it elementwise, with two inclusions inside each of the two biconditionals.

Proof (logical style).

Let $x$ be an object and write $a$ , $b$ , $c$ for the propositions $x \in A$ , $x \in B$ , $x \in C$ .

\begin{aligned} x \in A \cap A &\equiv a \land a \equiv x \in A && \text{by Idempotence} \\ x \in A \cap B &\equiv a \land b \equiv b \land a \equiv x \in B \cap A && \text{by Commutativity} \\ x \in (A \cap B) \cap C &\equiv (a \land b) \land c \\ &\equiv a \land (b \land c) \equiv x \in A \cap (B \cap C) && \text{by Associativity} \\ x \in A \cap (A \cup B) &\equiv a \land (a \lor b) \equiv x \in A && \text{by Absorption} \\ x \in A \cup (A \cap B) &\equiv a \lor (a \land b) \equiv x \in A && \text{by Absorption} \end{aligned}

Each chain is a biconditional for every $x$ , so Axiom 3.3 gives the corresponding equalities.

Proof (element style).

For the fifth part, suppose first that $A \cap B = A$ . Since $A \cap B \subset B$ by Proposition 3.32 , we get $A \subset B$ . Conversely, suppose $A \subset B$ . We have $A \cap B \subset A$ by Proposition 3.32 , and if $x \in A$ then $x \in B$ , so $x \in A \cap B$ ; hence $A \subset A \cap B$ , and Proposition 3.29 gives $A \cap B = A$ .

For the other equivalence, suppose $A \cup B = B$ . Then $A \subset A \cup B = B$ by Proposition 3.32 and substitution. Conversely, suppose $A \subset B$ . We have $B \subset A \cup B$ by Proposition 3.32 , and if $x \in A \cup B$ then $x \in A$ or $x \in B$ , and in either case $x \in B$ ; hence $A \cup B \subset B$ , and Proposition 3.29 gives $A \cup B = B$ . Both equivalences hold, so the three statements are equivalent.

Remark.

These identities, together with the complement laws, are what it means to say that the subsets of a fixed ambient set form a boolean algebra: the same structure the connectives $\neg$ , $\land$ and $\lor$ were shown to have in the first chapter, met a second time with sets in place of propositions.

Power Sets

Sets collect objects, and nothing forbids those objects from being sets themselves: here we collect all the subsets of one set into a single set, a construction we will meet far more often than its modest definition suggests.

Collecting the subsets of $A$ is not a case of comprehension, since it does not carve out of a set already in hand: the subsets of $A$ are not among the elements of $A$ , and there is no larger set on the table to cut them from. So the set has to be supplied.

Axiom 3.42 (Power set).

For every set $S$ there exists a set whose elements are exactly the subsets of $S$ : for all sets $X$ , $\forall S\,\exists P\,\forall X\,(X \in P \iff X \subset S)$ .

Definition 3.43 (Power set).

Let $A$ be a set. The power set of $A$ , written $\mathcal{P}(A)$ , is the unique set whose elements are exactly the subsets of $A$ : for every set $X$ , $X \in \mathcal{P}(A) \iff X \subset A$ . We also write it $\{X \mid X \subset A\}$ .

Remark.

That last notation is the unrestricted form we rejected earlier, and it is safe here only because the axiom has already produced the set. The braces are naming a set we hold; writing $\{X \mid X \subset A\}$ with no axiom behind it would lead us back to Russell.

Example 3.44.

Let $A = \{a, b\}$ with $a \neq b$ . Then $\mathcal{P}(A) = \bigl\{\emptyset, \{a\}, \{b\}, A\bigr\}$ . The elements of $\mathcal{P}(A)$ are sets, so we write $\{a\} \in \mathcal{P}(A)$ because $\{a\} \subset A$ , while $a \in \mathcal{P}(A)$ is simply false.

Proposition 3.45 (Power set of the empty set).

$\mathcal{P}(\emptyset) = \{\emptyset\}$ .

Discussion.

The claim is an equality of sets, so Proposition 3.29 lets us prove the two inclusions. For $\{\emptyset\} \subset \mathcal{P}(\emptyset)$ it is enough to check that $\emptyset$ is a member of the power set, which Definition 3.43 reduces to $\emptyset \subset \emptyset$ . For the reverse inclusion we take an arbitrary $X \in \mathcal{P}(\emptyset)$ ; the same definition converts that membership into $X \subset \emptyset$ , and since the empty set is a subset of every set we have $\emptyset \subset X$ as well, so mutual inclusion forces $X = \emptyset$ . The logical proof collapses the same chain into biconditionals: membership in the power set is the subset relation, which against $\emptyset$ is equality with $\emptyset$ , which is membership in $\{\emptyset\}$ .

Proof (element style).

( $\implies$ ) Since $\emptyset \subset \emptyset$ , Definition 3.43 gives $\emptyset \in \mathcal{P}(\emptyset)$ , and hence $\{\emptyset\} \subset \mathcal{P}(\emptyset)$ .

( $\impliedby$ ) Conversely, let $X \in \mathcal{P}(\emptyset)$ . Then $X \subset \emptyset$ , and since $\emptyset \subset X$ as well, Proposition 3.29 gives $X = \emptyset$ , so $X \in \{\emptyset\}$ . Thus $\mathcal{P}(\emptyset) \subset \{\emptyset\}$ , and the two inclusions give the equality.

Proof (logical style).

For every set $X$ ,

\begin{aligned} X \in \mathcal{P}(\emptyset) &\equiv X \subset \emptyset && \text{by the power set} \\ &\equiv X = \emptyset && \text{since } \emptyset \subset X \\ &\equiv X \in \{\emptyset\} && \text{by the singleton criterion} \end{aligned}

The biconditional holds for every $X$ , so Axiom 3.3 gives $\mathcal{P}(\emptyset) = \{\emptyset\}$ .

Theorem 3.46 (Power-set laws).

Let $A$ and $B$ be sets. Then

$\{\emptyset, A\} \subset \mathcal{P}(A)$ ;
$A \subset B$ if and only if $\mathcal{P}(A) \subset \mathcal{P}(B)$ ;
$\mathcal{P}(A) \cup \mathcal{P}(B) \subset \mathcal{P}(A \cup B)$ ;
$\mathcal{P}(A) \cap \mathcal{P}(B) = \mathcal{P}(A \cap B)$ .

Discussion.

Every claim reduces to Definition 3.43 : a set belongs to a power set exactly when it is a subset of the set in question. The first is immediate from $\emptyset \subset A$ and $A \subset A$ . The second is a biconditional, so it splits: forwards, an $X \in \mathcal{P}(A)$ has $X \subset A$ and $A \subset B$ , and Proposition 3.28 chains them; backwards, the first part puts $A$ itself into $\mathcal{P}(A)$ , so an inclusion of power sets hands us $A \in \mathcal{P}(B)$ , which is $A \subset B$ read back through the definition. The third is one inclusion only, since a subset of $A$ or of $B$ is a subset of $A \cup B$ either way, and the reverse fails in general, as the example after the proof shows. The fourth is an equality, so both inclusions, and it holds because being a subset of both $A$ and $B$ is the same thing as being a subset of $A \cap B$ .

Proof.

For the first claim, $\emptyset \subset A$ and $A \subset A$ , so $\emptyset \in \mathcal{P}(A)$ and $A \in \mathcal{P}(A)$ by Definition 3.43 , and therefore $\{\emptyset, A\} \subset \mathcal{P}(A)$ .

For the second, suppose $A \subset B$ and take $X \in \mathcal{P}(A)$ . Then $X \subset A$ , and with $A \subset B$ this gives $X \subset B$ by Proposition 3.28 , so $X \in \mathcal{P}(B)$ . Hence $\mathcal{P}(A) \subset \mathcal{P}(B)$ . Conversely, suppose $\mathcal{P}(A) \subset \mathcal{P}(B)$ . The first claim gives $A \in \mathcal{P}(A)$ , so $A \in \mathcal{P}(B)$ and therefore $A \subset B$ .

For the third, let $X \in \mathcal{P}(A) \cup \mathcal{P}(B)$ , so $X \in \mathcal{P}(A)$ or $X \in \mathcal{P}(B)$ by Proposition 3.21 . If $X \in \mathcal{P}(A)$ then $X \subset A$ , and every element of $X$ then lies in $A$ and so in $A \cup B$ ; if $X \in \mathcal{P}(B)$ the same argument runs through $B$ . Either case gives $X \subset A \cup B$ , that is, $X \in \mathcal{P}(A \cup B)$ .

For the fourth, let $X \in \mathcal{P}(A) \cap \mathcal{P}(B)$ . Then $X \subset A$ and $X \subset B$ , so every element of $X$ lies in $A$ and in $B$ , hence in $A \cap B$ . Thus $X \subset A \cap B$ and $X \in \mathcal{P}(A \cap B)$ . Conversely, let $X \in \mathcal{P}(A \cap B)$ . Every element of $X$ lies in $A \cap B$ and so lies in $A$ , and equally in $B$ , giving $X \subset A$ and $X \subset B$ . Hence $X$ belongs to both $\mathcal{P}(A)$ and $\mathcal{P}(B)$ , and therefore to their intersection.

Example 3.47.

The inclusion in the third claim really can be strict. Let $A = \{a\}$ and $B = \{b\}$ with $a \neq b$ . Then $\{a, b\} \subset A \cup B$ , so $\{a, b\} \in \mathcal{P}(A \cup B)$ , but $\{a, b\}$ is a subset of neither $A$ nor $B$ and so lies in neither $\mathcal{P}(A)$ nor $\mathcal{P}(B)$ .

Problem 3.11.

Let $A$ be a set and let $x$ be an object with $x \notin A$ . Describe $\mathcal{P}(A \cup \{x\})$ in terms of $\mathcal{P}(A)$ .

Problem 3.12.

Can $\mathcal{P}(A) \setminus \mathcal{P}(B)$ ever be the power set of some set? Prove your answer.

Problem 3.13.

Find a necessary and sufficient condition on $A$ and $B$ for $\mathcal{P}(A \setminus B) = \mathcal{P}(A)$ , and prove that your condition works in both directions.

Replacement

Everything we have built so far either cuts a set down or pools sets together. Nothing we have assumed lets us take a set and change what is in it. Suppose we hold $\{3, 5, 9\}$ and want the set holding one more than each of those, $\{4, 6, 10\}$ : comprehension carves out of a set we are holding, and none of $4$ , $6$ , $10$ lies in $\{3, 5, 9\}$ , so there is nothing to carve them from. The axiom below closes that gap by letting a statement pair each element with its replacement.

Axiom 3.48 (Replacement).

Let $A$ be a set, and let $P(x, y)$ be a statement about an object $x \in A$ and an object $y$ such that for each $x \in A$ there is at most one $y$ making $P(x, y)$ true. Then there exists a set $B$ whose elements are exactly those partners: for any object $z$ ,

z \in B \iff P(x, z) \text{ for some } x \in A.

The condition that each $x$ have at most one partner is what keeps the axiom honest. A statement free to pair one $x$ with many $y$ could sweep in everything in sight, and we would be back with the unrestricted notation and its paradox; tying each element to a single partner means every object in the new set is the partner of something in $A$ , so nothing enters that $A$ did not put there.

Example 3.49.

Take $A = \{3, 5, 9\}$ and let $P(x, y)$ be the statement $y = x + 1$ . Each $x$ in $A$ has exactly one partner, so the axiom applies, and the set it hands back is $\{4, 6, 10\}$ .

Example 3.50.

Take $A = \{3, 5, 9\}$ again, and let $P(x, y)$ be the statement $y = 1$ . Each $x$ in $A$ still has exactly one partner, but it is the same partner every time, so the set produced is $\{1\}$ . The axiom may return something smaller than what we started with, since nothing forces distinct elements to have distinct partners.

Axiom 3.3 makes that $B$ unique, so we may name it, and we write it $\{y : P(x, y) \text{ for some } x \in A\}$ . As with the power set, those braces carry no carving set and are safe for the same reason: the axiom produced the set before the notation named it. When the partner of $x$ is written $f(x)$ we abbreviate further, to $\{f(x) : x \in A\}$ or $\{f(x) \mid x \in A\}$ .

We promised at the outset that our axioms would be overcomplete.

Proposition 3.51 (Comprehension from replacement).

Let $A$ be a set and $Q$ a predicate. Then replacement alone produces a set whose elements are exactly the elements of $A$ for which $Q$ holds.

Discussion.

Replacement builds a set by transforming elements, while comprehension builds one by selecting them, so the work is to make a transformation do the selecting. We transform each element into itself, and only when $Q$ holds of it: the statement $P(x, y)$ saying ” $x = y$ and $Q(x)$ ” pairs an element satisfying $Q$ with itself and leaves an element failing $Q$ with no partner at all. The at-most-one condition is then met for a reason worth noticing, since some elements have no partner rather than one, and the set of partners is exactly the set of elements we wanted to keep.

Proof.

Let $P(x, y)$ be the statement ” $x = y$ and $Q(x)$ ”, and let $x \in A$ . If $Q(x)$ holds, the only $y$ with $P(x, y)$ is $x$ itself; if $Q(x)$ fails, no $y$ satisfies $P(x, y)$ . Either way there is at most one such $y$ , so Axiom 3.48 applies and produces a set $B$ with $z \in B$ exactly when $P(x, z)$ holds for some $x \in A$ .

Suppose $z \in B$ . Then some $x \in A$ has $x = z$ and $Q(x)$ , so $z \in A$ by substitution, and $Q(z)$ likewise. Conversely, if $z \in A$ and $Q(z)$ , then $x = z$ is itself a witness, so $z \in B$ . Hence $z \in B \iff (z \in A \land Q(z))$ for every object $z$ , which is the criterion of $\{x \in A \mid Q(x)\}$ .

So Axiom 3.8 could have been left out. We keep it anyway, and that is an editorial choice rather than anything the proposition settles: the discussion of Russell’s paradox turned on carving into a set we already hold, and it is the axiom we reach for constantly. The two also combine, so to build $\{f(x) : x \in A,\ P(x)\}$ we first form $\{x \in A \mid P(x)\}$ by comprehension and then apply replacement to it.

Remark.

Replacement is a schema, as comprehension is: one axiom for each statement $P$ , not a single statement quantifying over all of them.

Regularity (Optional)

Our set-builder notation was rejected for producing a set that could not exist. The damage runs further than that one set: unrestricted, the notation also hands us the collection of every object at once, and since sets are objects by Axiom 3.2 , such a collection would contain itself. A box holding itself is not something the picture we started from can draw.

The intuition that keeps this from happening is that objects come in stages. At the bottom sit the objects that are not sets at all, such as the number $37$ . Above them sit the sets built only from those, like $\{3, 4, 7\}$ and $\emptyset$ . Above those sit the sets built from everything so far, like $\{3, 4, 7, \{3, 4, 7\}\}$ , and so on upward. A box at any stage holds only boxes opened at earlier stages, so no box ever ends up inside itself.

Writing that hierarchy down properly is a good deal of work, and we will not do it. We take instead the one consequence of it we need.

Axiom 3.52 (Regularity).

If $A$ is a non-empty set, then at least one element of $A$ is either not a set, or is disjoint from $A$ .

Read against the hierarchy, the axiom says that some element of $A$ sits low enough to hold none of the others. It asks this of one element only, not of all of them.

Example 3.53.

Let $A = \bigl\{\{3, 4\},\ \{3, 4, \{3, 4\}\}\bigr\}$ . Its first element $\{3, 4\}$ holds neither of the elements of $A$ , since neither $3$ nor $4$ lies in $A$ , so it is disjoint from $A$ and the axiom is satisfied. The second element sits a stage higher and does hold an element of $A$ , namely $\{3, 4\}$ , which the axiom permits.

Problem 3.14.

Show that the unrestricted notation of the set-builder section, had we assumed it rather than rejected it, would imply Axiom 3.8 , Axiom 3.14 , Axiom 3.18 , Axiom 3.42 and Axiom 3.48 , and would therefore have spared us most of this chapter.

Problem 3.15.

Use regularity, together with Axiom 3.14 , to show that $A \notin A$ for every set $A$ . Show further that for any two sets $A$ and $B$ , either $A \notin B$ or $B \notin A$ , or both.

Problem 3.16.

Show, assuming the other axioms, that the unrestricted notation is equivalent to postulating a set $\Omega$ containing every object: if the notation is permitted then such an $\Omega$ exists, and if such an $\Omega$ exists then the notation is legitimate.

The second problem is worth a second look once it is done. It says that for any set $A$ there is always an object outside $A$ , namely $A$ itself, so we may always add one more element and form the larger set $A \cup \{A\}$ . It also gives a second route to Proposition 3.13 , since a set $\Omega$ holding every object would hold itself, which regularity forbids. We proved that proposition from comprehension alone, so the two arguments lean on nothing in common.

Remark.

One may fairly ask whether we need this axiom, since it is less intuitive than the others. For analysis we do not: the sets we meet are all low in the hierarchy, sets of ordinary objects or sets of those, and nothing later in these notes depends on regularity. It matters for set theory pursued for its own sake, and we state it here so the list is complete.

Exercises

Answers are checked in your browser, as often as you like. Nothing is sent anywhere and nothing is kept but your own work. A formula may be written with the symbols themselves or with ~ & | -> <-> ^, and \and, \or, \to expand as you type.

Exercises in Lean

The proofs below are checked in your browser. Nothing is sent anywhere, and nothing is stored but your own work. Type \to for →, \and for ∧, \< and \> for ⟨ ⟩.

The last two sheets were about statements. This one is about objects, and about the sets that hold them.

The editor has one type, Obj, and its terms are the objects of this chapter. Sets are objects too by Axiom 3.2 , so a set and its elements are terms of that same type, and x ∈ A is a statement about any two of them. Nothing marks off the objects that are sets from those that are not, and every exercise below is about sets.

The notation is typed with the backslash abbreviations: \in for ∈, \nin for ∉, \sub for ⊆, \cup for ∪, \cap for ∩, \emptyset for ∅ and \powerset for 𝒫. The difference A \ B is a plain backslash.

Inclusion

An inclusion is not a new kind of statement. A ⊆ B is ∀ x, x ∈ A → x ∈ B written short, so it is proved the way an implication is, by intro, and used the way an implication is, by applying it: with h : A ⊆ B and hx : x ∈ A, the term h x hx proves x ∈ B. A goal ∀ x, p x behaves the same way, intro x fixing an arbitrary x and leaving p x.

Example.

An inclusion applied to an object and to a proof that the object lies in the smaller set.

The operations are nothing more than their membership criteria. x ∈ A ∪ B is the disjunction x ∈ A ∨ x ∈ B, not merely equivalent to it, so left, right and rcases work on a membership in a union as they do on any disjunction. x ∈ A ∩ B is the conjunction x ∈ A ∧ x ∈ B, so ⟨_, _⟩ builds one and .left and .right take one apart.

Example.

The first intro fixes the object, the second assumes it lies in $A$ .

Example.

Half of a conjunction, reached through the criterion for the intersection.

Exercise 3.10.

Both criteria at once: take the conjunction apart, then choose a side of the disjunction.

Exercise 3.11.

Subsets are transitive.

Exercise 3.12.

A set containing both $A$ and $B$ contains their union.

Exercise 3.13.

And a set contained in both is contained in their intersection.

Equality

Two sets are equal when they have the same elements, and Set.ext is that axiom: handed ∀ x, x ∈ A ↔ x ∈ B it returns A = B. So apply Set.ext turns a goal A = B into that biconditional, intro x fixes the object, and constructor splits the biconditional into its two directions.

Example.

Idempotence of the intersection, which is idempotence of $\land$ underneath.

Mutual inclusion says the same thing, and Set.subset_antisymm is Proposition 3.29 . Applying it leaves the two inclusions as separate goals, which is often the shorter road, since neither of them mentions the biconditional.

Example.

Absorption. The harder inclusion splits on the union; the other one is a line.

`have`

A proof that needs a step of its own records it with have. Writing have h : p := … adds h : p to the context, and what follows := is either a term or by with a block indented under it.

Example.

The intermediate membership is named, and then taken apart.

Exercise 3.14.

The order of a union carries no information.

Exercise 3.15.

The distributive law left unproved in Theorem 3.40 .

Difference

x ∈ A \ B is x ∈ A ∧ ¬(x ∈ B), a conjunction whose right half is a negation, which is to say a function into False.

Example.

The negative half, taken out of the conjunction.

And x ∈ ∅ is False itself. There is nothing to do with such a hypothesis but close the branch, which h.elim does, proving whatever the goal happens to be.

Example.

Nothing lies in the empty set, so this branch never arises.

Exercise 3.16.

Taking $A$ out of $B$ first costs the union nothing.

Exercise 3.17.

De Morgan’s second law, with the complement written as a difference.

Exercise 3.18.

Its companion.

Symmetric difference

For sets $A$ and $B$ , the symmetric difference $A \oplus B$ is $(A \setminus B) \cup (B \setminus A)$ , the set of objects belonging to exactly one of the two. The editor has no notation for it, so the statements below carry it written out.

An equation between sets is used with rw: from h : A = B, rw [h] replaces $A$ by $B$ in the goal, and rw [h] at k does it inside the hypothesis k.

Example.

Substitution, which is what an equation is for.

Exercise 3.19.

$A \oplus A = \emptyset$ .

Exercise 3.20.

$A \oplus \emptyset = A$ .

Exercise 3.21.

$(A \oplus B) \setminus (A \setminus B) = B \setminus A$ .

Exercise 3.22.

If $A \oplus B$ is empty then $A$ and $B$ are the same set.

Power sets

X ∈ 𝒫 A is X ⊆ A, which is a ∀ again, so a membership in a power set opens with intro like any other inclusion.

Example.

Every set is a subset of itself, and so an element of its own power set.

Exercise 3.23.

Half of Theorem 3.46 , part two.

Exercise 3.24.

And part four of it.

Exercise 3.25.

Since $\mathcal{P}(\emptyset)$ is $\{\emptyset\}$ , this is the inclusion $\mathcal{P}(A \setminus B) \subset \bigl(\mathcal{P}(A) \setminus \mathcal{P}(B)\bigr) \cup \{\emptyset\}$ .

What the checker understands

Tactics

intro h	assume the hypothesis of an implication, naming it h
exact e	give the proof outright
apply f	reduce the goal to the hypotheses of f
assumption	close the goal with a hypothesis already present
trivial	close the goal True
exfalso	replace the goal with False
by_contra h	assume the negation of the goal
constructor	split ∧ into both halves, or ↔ into both directions
left / right	choose which half of a ∨ to prove
rcases h with a \| b	argue by cases on a disjunction
obtain ⟨a, b⟩ := h	take a conjunction or an existential apart
cases h	as above, keeping the name
refine e	give the proof with holes left in it
have h : p := …	record an intermediate result
show p	restate the goal in an equal form
use w	give a witness for ∃
specialize h a	instantiate a ∀ hypothesis
rw [h]	rewrite with an equation, ← to go backwards
rfl	both sides compute to the same thing
decide / norm_num	settle a closed computation

Results you may cite

Classical.em	∀ (a : Prop), a ∨ ¬a — the law of excluded middle
Classical.byContradiction	∀ {a : Prop}, (¬a → False) → a — proof by contradiction; the tactic by_contra does this for you
Classical.byCases	∀ {a b : Prop}, (a → b) → (¬a → b) → b — split on whether a holds
not_not	∀ {a : Prop}, ¬¬a ↔ a — double negation
not_and_or	∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b — De Morgan
not_or	∀ {a b : Prop}, ¬(a ∨ b) ↔ ¬a ∧ ¬b — De Morgan
not_imp	∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
and_comm	∀ {a b : Prop}, a ∧ b ↔ b ∧ a
or_comm	∀ {a b : Prop}, a ∨ b ↔ b ∨ a
Set.ext	∀ {A B : Obj}, (∀ x : Obj, x ∈ A ↔ x ∈ B) → A = B — extensionality: sets with the same elements are equal
Set.ext_iff	∀ {A B : Obj}, A = B ↔ (∀ x : Obj, x ∈ A ↔ x ∈ B) — extensionality and substitution, in one biconditional
Set.subset_antisymm	∀ {A B : Obj}, A ⊆ B → B ⊆ A → A = B — mutual inclusion is equality
Set.empty_subset	∀ {A : Obj}, ∅ ⊆ A — the empty set is a subset of every set

From the logical core

And.intro	∀ {a b : Prop}, a → b → a ∧ b
And.left	∀ {a b : Prop}, a ∧ b → a
And.right	∀ {a b : Prop}, a ∧ b → b
And.symm	∀ {a b : Prop}, a ∧ b → b ∧ a
Or.inl	∀ {a b : Prop}, a → a ∨ b
Or.inr	∀ {a b : Prop}, b → a ∨ b
Or.elim	∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
Or.symm	∀ {a b : Prop}, a ∨ b → b ∨ a
Iff.intro	∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.mp	∀ {a b : Prop}, (a ↔ b) → a → b
Iff.mpr	∀ {a b : Prop}, (a ↔ b) → b → a
Iff.symm	∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
Iff.rfl	∀ {a : Prop}, a ↔ a
Iff.trans	∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
True.intro	True
False.elim	∀ {a : Prop}, False → a
absurd	∀ {a b : Prop}, a → ¬a → b
id	∀ {a : Prop}, a → a
mt	∀ {a b : Prop}, (a → b) → ¬b → ¬a
Eq.refl	∀ {α : Type} (a : α), a = a
Eq.symm	∀ {α : Type} {a b : α}, a = b → b = a
Eq.trans	∀ {α : Type} {a b c : α}, a = b → b = c → a = c
congrArg	∀ {α : Type} {β : Type} {a b : α} (f : α → β), a = b → f a = f b
Exists.intro	∀ {α : Type} {p : α → Prop} (w : α), p w → ∃ x : α, p x
Exists.elim	∀ {α : Type} {p : α → Prop} {b : Prop}, (∃ x : α, p x) → (∀ y : α, p y → b) → b