Solutions to the Set Theory Exercises

2. Defining union

Definition: y = Uz <---> Ax(x in y <---> Ew (w in z & x in w)).

Existence proof:

1. Az Ey Ax (x in y & Ew (w in z & x in w) ---> x in y) [union axiom, AE]

Uniqueness proof:

1. | (x in y <---> Ew (w in z & x in w))
2. | (x in y' <---> Ew (w in z & x in w))
3. | x in y <---> x in y'
4. | Ax (x in y <---> x in y')
5. | Ax (x in y <---> x in y') ---> y = y' [axiom of extensionality]
6. | y = y'
7. (x in y <---> Ew (w in z & x in w)) ---> y = y'

Equational Definitions

Let t(x) be an introduced term.

Let f(x) = y <---> y = t(x) be a definition.

Generic proof of existence for a definition in terms of a term

1. y = t(x)
2. Ez y = z [EI]

Generic proof of uniqueness for such a definition

1. | y = t(x) & y' = t(x)
2. | y = y' [=]
3. y = t(x) & y' = t(x) ---> y = y'

From now on, you don't have to justify definitions in terms of identity with terms.

Incidentally, a definition in terms of a term may be equivalently rephrased as an equation:

f(x) = y <---> y = t(x)

is logically equivalent to

f(x) = t(x)

Proof:

1. | f(x) = t(x)
2. | | f(x) = y
3. | | y = t(x) [=]
4. | f(x) = y ---> y = t(x)
5. | | y = t(x)
6. | | f(x) = y
7. | y = t(x) ---> f(x) = y
8. | y = t(x) <---> f(x) = y
9. f(x) = t(x) ---> (y = t(x) <---> f(x) = y)
10. | y = t(x) <---> f(x) = y
11. | Ay(y = t(x) <---> f(x) = y) [AI]
12. | t(x) = t(x) <---> f(x) = t(x)) [AE]
13. | t(x) = t(x)
14. | f(x) = t(x)
15. (y = t(x) <---> f(x) = y) ---> f(x) = t(x)
16. (y = t(x) <---> f(x) = y) <---> f(x) = t(x)

1. Defining Intersection

Intersect(z) = {x in Uz: Aw(w in z ---> x in w)}.

3. Defining x U y

x U y = U{x, y}

4. Replacement: as usual.

5. Show that

-Es s is a function & Ax, y, (x, y> in s <---> u = x U {x}

Proof

1. | Es s is a function & Ax, y, (<x, y> in s <---> y = x U {x}) [hyp]
2. | | s is a function & Ax, y, (<x, y> in s <---> y = x U {x}) [hyp]
3. | | x in dom(s) <---> Ey <x, y> in s [defn dom]
4. | | x in dom(s) <---> Ey y = x U {x} [logic]
5. | | x in dom(s) [logic]
6. | | Ax x in dom(s) [logic]
7. | | Ey Ax x in y [EI]
8. | Ey Ax x in y [EE]
9. | _|_ [Russell's paradox using separation]