# Nested Quantifiers

Our examples so far have included propositions with single quantifiers. This section will discuss how to prove sequents that use nested quantifers. We will see that the approach is the same as before, but that we must take caution to process the quantifiers in the correct order. Recall that quantifier precedence is from right to left (i.e., from the outside in), so that `∀ x ∀ y P(x, y)`

is equivalent to `∀ x (∀ y P(x, y))`

.

## Example 1

Suppose we wish to prove the following sequent:

`∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)`

Since we wish to prove a for-all statement of the form `∀ y (SOMETHING)`

, then we know we must start with our for all introduction template:

```
∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
1. ∀ x ∀ y P(x, y) premise
2. {
3. a
//need: ∀ x P(a, x)
}
//want to use ∀i to conclude ∀ y ∀ x P(y, x)
}
```

But now we see that we want to prove ANOTHER for-all statement, `∀ x P(a, x)`

. So we again use our for all introduction strategy in a nested subproof:

```
∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
1. ∀ x ∀ y P(x, y) premise
2. {
3. a
4. {
5. b
//need: P(a, b)
}
//want to use ∀i to conclude ∀ x P(a, x)
//need: ∀ x P(a, x)
}
//want to use ∀i to conclude ∀ y ∀ x P(y, x)
}
```

Now, in subproof 4, we see that we must use `∀e`

on our premise (`∀ x ∀ y P(x, y)`

) to work towards our goal of `P(a, b)`

. We have two available individuals – `a`

and `b`

. When we use `∀e`

, we must eliminate the OUTER (top-level) quantifier and its variable. In the case of `∀ x ∀ y P(x, y)`

, we see that we must eliminate the `∀ x`

. Since the `x`

is the first parameter in `P(x, y)`

, and since we are hoping to reach `P(a, b)`

by the end of subproof 4, we can see that we need to plug in the `a`

for the `x`

so that it will be in the desired position:

```
∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
1. ∀ x ∀ y P(x, y) premise
2. {
3. a
4. {
5. b
6. ∀ y P(a, y) ∀e 1 a
//need: P(a, b)
}
//want to use ∀i to conclude ∀ x P(a, x)
//need: ∀ x P(a, x)
}
//want to use ∀i to conclude ∀ y ∀ x P(y, x)
}
```

Note that on line 6, we could NOT have used `∀e`

to eliminate the `∀ y`

in `∀ x ∀ y P(x, y)`

, as it was not the top-level operator.

Next, we apply `∀e`

again to `∀ y P(a, y)`

to leave us with `P(a, b)`

. All that remains at that point is to use `∀i`

twice as planned to wrap up the two subproofs. Here is the completed proof:

```
∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
1. ∀ x ∀ y P(x, y) premise
2. {
3. a
4. {
5. b
6. ∀ y P(a, y) ∀e 1 a
7. P(a, b) ∀e 6 b
//need: P(a, b)
}
//want to use ∀i to conclude ∀ x P(a, x)
8. ∀ x P(a, x) ∀i 4
//need: ∀ x P(a, x)
}
//want to use ∀i to conclude ∀ y ∀ x P(y, x)
9. ∀ y ∀ x P(y, x) ∀i 2
}
```

## Example 2

Suppose we have the predicate `IsBossOf(x, y)`

in the domain of people, which describes whether person `x`

is the boss of person `y`

. We wish to prove the following sequent:

`∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)`

You can read the premise as “There is a person that is everyone’s boss”. From this statement, we are trying to prove the conclusion: “All people have a boss”. Here is the completed proof:

```
∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)
{
1. ∃ x ∀ y IsBossOf(x, y) premise
2. {
3. a ∀ y IsBossOf(a, y) assume
4. {
5. b
6. IsBossOf(a, b) ∀e 3 b
7. ∃ x IsBossOf(x, b) ∃i 6 a
}
8. ∀ y ∃ x IsBossOf(x, y) ∀i 4
}
9. ∀ y ∃ x IsBossOf(x, y) ∃e 1 2
}
```

In the above proof, we let `a`

be our made-up name for the boss-of-everyone. So, we have the assumption that `∀ y IsBossOf(a, y)`

. Next, we let `b`

be “anybody at all” who we might examine in the domain of people. The proof exposes that the boss of “anybody at all” in the domain must always be `a`

. `∀i`

and then `∃e`

finish the proof.

Here is the proof worked again, with the subproofs swapped:

```
∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)
{
1. ∃ x ∀ y IsBossOf(x, y) premise
2. {
3. b
4. {
5. a ∀ y IsBossOf(a, y) assume
6. IsBossOf(a, b) ∀e 5 b
7. ∃ x IsBossOf(x, b) ∃i 6 a
}
8. ∃ x IsBossOf(x, b) ∃e 1 4
}
9. ∀ y ∃ x IsBossOf(x, y) ∀i 2
}
```

Can we prove the converse? That is, if everyone has a boss, then there is one boss who is the boss of everyone?

`∀ y ∃ x IsBossOf(x, y) ⊢ ∃ x ∀ y IsBossOf(x, y)`

NO. We can try, but we get stuck:

```
∀ y ∃ x IsBossOf(x, y) ⊢ ∃ x ∀ y IsBossOf(x, y)
{
1. ∀ y ∃ x IsBossOf(x, y) premise
2. {
3. a
4. ∃ x IsBossOf(x, a) ∀e 1 a
5. {
6. b IsBossOf(b, a) assume
}
7. ∀ y isBoss(b, y) ∀i 2 NO--THIS PROOF IS TRYING TO FINISH
THE OUTER SUBPROOF WITHOUT FINISHING
THE INNER ONE FIRST.
...can't finish
}
```

We see that the “block structure” of the proofs warns us when we are making invalid deductions.