## Exercise statement

Let be sets. Define a *partial function* from to to be any function whose domain is a subset of , and whose range is a subset of . Show that the collection of all partial functions from to is itself a set.

## Hints

- Use Exercise 3.4.6, the power set axiom, the replacement axiom, and the union axiom.

## How to think about the exercise

If and , then we can form the set using the power set axiom; this gives us all of the partial functions with domain and range . Now we just want to “loop over” all combinations of , and take the union to “flatten” the result. In other words, we want the set

But we are not yet done, because we must justify all of the steps using the axioms and results we have so far.

First of all, to use the replacement axiom, we need the “looping over” construct to use the “is an element” relation rather than the “is a subset” relation, i.e. to be in the form rather than as above. This is easy to fix: by Lemma 3.4.9, the sets and exist, so the set we want is

Now we run into the problem that the replacement axiom only allows us to “loop over” a single set, so we can’t be looping over the sets and simultaneously. To turn this double loop into a single loop, we can use the notion of *ordered pairs* and the *Cartesian product*; but it turns out that in this book, these ideas are only introduced in section 3.5, the next section! If we cheat a little and use these ideas, then the set exists. Now we can use the replacement axiom to replace each ordered pair by the set . In other words, we have the set

I consider this an entirely acceptable solution to this exercise: it is the natural, obvious thing one comes up with. Alternatively, if this solution isn’t acceptable, then I consider this exercise to be pretty unfair! With that complaint out of the way, let’s see if we can find a different solution that does not require Cartesian products.

So, we can only loop over one set at a time, and we aren’t allowed to take the Cartesian product to compress the double loop into a single loop. What to do? If you are familiar with computer programming, you might at this point have an idea.

In Python, given a list `X = [1,2,3]`

and another list `Y = [4,5]`

, how can we print all of the ordered pairs `(x, y)`

where `x`

is in `X`

and `y`

is in `Y`

? One idea is to use the Cartesian product functionality that is provided by the language:

from itertools import product
for p in product(X, Y):
print(p)
# prints the following:
# (1, 4)
# (1, 5)
# (2, 4)
# (2, 5)
# (3, 4)
# (3, 5)

But more obvious idea is to just use a nested loop:

for x in X:
for y in Y:
print((x, y))
# prints the following:
# (1, 4)
# (1, 5)
# (2, 4)
# (2, 5)
# (3, 4)
# (3, 5)

(Aside for people who know Haskell: You can think of `[(x,y) | x <- [1,2,3], y <- [4,5]]`

versus `[[(x,y) | y <- [4,5]] | x <- [1,2,3]]`

; the latter must be flattened using `concat`

, analogously to how we must apply union twice below. Consider also currying, e.g. the difference between `add :: (Int, Int) -> Int; add (x,y) = x+y`

and `add' :: Int -> (Int -> Int); add' = \x -> (\y -> x+y)`

. The former eats both arguments at once while the latter eats one argument, spitting out a function which can eat an argument. This gives us a way to define functions which can essentially take multiple arguments, without actually taking multiple arguments, analogously to how here we want to simulate taking from multiple sets without actually taking from multiple sets at once.)

The benefit of the nested loop, for our purposes, is that we are only looping over a single list or set at a time, so the axiom of replacement can be applied. How will this work? First, fix a set . Then we can form the set using the replacement axiom. This gives us all of the partial functions with domain . Now we just need to loop over all of the possible domains, by forming the set . But since we formed these sets in stages, we must now take the union twice (instead of once, as we did in our first solution above) to “flatten” this set, so our final answer is .

Let’s take an example to make sure this actually works. Let and . Then we have and . The partial functions from to are the following:

- : Domain and range , which is an empty function.
- : Domain and range , which is an empty function.
- : Domain and range , which is an empty function.
- : Domain and range , which is an empty function.
- : Domain and range , which maps .
- : Domain and range , which maps .
- : Domain and range , which maps .
- : Domain and range , which maps .

Let’s first check the sets for a fixed . The subsets of are and so we have

and

Now, the set is equal to , which by the above computation is just . Taking the union once gives us , and taking the union again gives us , which is precisely what we wanted.

You’ve probably noticed that we could have taken the union at an intermediate stage: and . So we can form the set , which equals ; taking the union again then gives us the same answer. In the solution below we will use this latter expression.

This is one of those exercises where it can be difficult to tell when one is done (alternatively, the difficulty depends a lot on where one decides one is “off the hook”). I can easily imagine people skipping the proof that the resulting set is actually the set of all partial functions, for example.

## Model solution

By Lemma 3.4.9, the sets and exist. Fix some subset of . Then the set exists by the power set axiom and replacement axiom. (Formally, we can proceed as follows. Let be the predicate , pertaining to sets . If is a set, then exists by the power set axiom. Thus for each there is exactly one (hence at most one) such that . Thus by the replacement axiom the set exists.)

By the union axiom, the set exists. By the replacement axiom again, the set exists. (Formally, we can define the predicate by .)

By the union axiom again, the set exists. It remains to show that this set is the set of all partial functions from to . Let be an element of this set. Then by the union axiom, this means for some . By the replacement axiom, for some . Thus for some . By the union axiom, this means for some . By the replacement axiom, for some . Thus for some and . This means is a function from to , which means it is a partial function from to . This shows that every element of is a partial function from to .

Conversely, we now show that every partial function from to is in the set . Let be a function, where and . Then . Thus for some , since . If we define , then . Thus we have for some , which means that . Since , we thus see that for some . If we define , then . Thus we have for some , which means that . This is what we wanted to show, so we are done.