# Quantifiers and Derivations

Now that we have added quantifiers to our language, it’s time to learn how to reason with them.

## Universal Instantiation, Existential Generalization

In order to express rules for our quantifiers, we will need to do something to the symbols *ϕ* and *ψ* that lets us pay special attention to variables. So, we allow for the following convention. *ϕ*_{x} is a sentence where we are paying special attention to the free (not bound by any quantifier in *ϕ*_{x}) occurrences of the variable *x*. *ϕ*_{x}(*c*) is a sentence where we have replaced every free occurrence of the variable *x* with an occurrence of a constant *c*. So, *ϕ*_{x} might contain some occurrences of *c*. But *ϕ*_{x}(*c*) will not contain any free occurrences of *x*.

The two simplest rules for us to learn with the quantifiers are as follow:

- Universal Instantiation and Existential Generalization
*Universal Instantiation*(abbreviated UI), the argument form

∀

*x**ϕ*_{x}⊢*ϕ*_{x}(*c*)is a rule of direct inference

*Existential Generalization*(abbreviated EG), the argument form

*ϕ*_{x}(*c*)⊢∃*x**ϕ*_{x}

The basic idea behind each one is very simple. Universal instantiation takes note of the fact that if something is true of *everything*, then it must also be true of whatever particular thing is named by the constant *c*. Existential generalization takes note of the fact that if something is true of a particular constant *c*, then it’s at least true of *something*.

### Problem Set 16

Try out these new rules in the following derivations:

## Universal and Existential Derivations

You may have noticed that, while universal instantiation lets you reason *from* a universal statement, it will not let you prove any new universal statements. Similarly, while existential generalization will let you reason *to* existential statements, it does not let you use an existential statement to prove something new.

In other words, universal instantiation is an elimination rule for ∀, letting you eliminate universal statements, while existential generalization is an introduction rule for ∃, letting you introduce new existential statements. What we need, to complete the picture, is an introduction rule for ∀, and an elimination rule for ∃.

### Universal Derivation

We’ll discuss the introduction rule for ∀ first. How can you prove that some statement like “it is good” is true of absolutely everything? If we needed to prove it of two things, or three things, we could prove it of each of those things individually. But we clearly can’t go, one by one, through the collection of all things that exist and prove this statement of each one.

What we will do instead, is produce a kind of *proof recipe*. Our proof recipe will be such that, no matter what object we’re given, we could apply the recipe to show that the statement we’re trying to prove holds of everything holds of that given thing.

Here’s how this will work. We will need the idea of a *fresh* constant

- Fresh Constant
A constant is

*fresh*at a certain point in a proof if the constant does not appear in the premises of the proof, or on any earlier line (including show lines).

The idea is this: since a fresh constant is unrelated to anything from before, it could be interpreted to refer to anything at all. The new constant refers to an “arbitrary object” in the sense that nothing we’re assuming about it rules out the possibility that it could refer to anything we choose.

To prove our universal statement, we’ll begin with a show line, like “Show: ∀*x**φ*_{x}”, indicating the universal statement that we intend to show. We’ll then attempt to show that the statement applies to a fresh constant. If we succeed, producing a line like “ *φ*_{x}(*c*)”, where *c* is fresh at the show line, then what we have is a proof recipe. We know how to prove that *φ*_{x} applies to any give object at all, since we could just take our fresh constant to refer to that given object. Hence, we can cite the line where we produced *φ*_{x}(*c*) to close our universal derivation, writing UD to close it.

For example, the argument ⊢∀*x*(*F*(*x*)→*F*(*x*)) is valid:

```
1. Show: Ax(F(x)->F(x))
2. Show:F(c)->F(c)
3. F(c):PR
4. :CD 3
5. :UD 2
```

So is the argument ∀*x*(*F*(*x*)∧*G*(*x*)) ⊢ ∀*x**F*(*x*).

```
1. Show: Ax(F(x)/\G(x))
2. Ax(F(x)/\G(x)):PR
3. F(c)/\G(c):UI 2
4. F(c):S 3
5. :UD 4
```

### Problem Set 17

Please complete the following derivations:

Note that the problem set continues below.

### Existential Derivation

Universal Derivations give us a way of proving new universal statements. Existential derivations, on the other hand, give us a way of proving things by using existential statements.

The idea is this: if we know that *φ*_{x} is true of *something*, then we may reasonably give that something a temporary name. The only constraint is that, when we name this object, we must use a fresh constant to name it. This prevents us from illegitimately assuming that we know more about this object than simply that *φ*_{x} is true of it.

To prove something using an existential statement of the form ∃*x**ϕ*_{x}, we’ll begin with a show line, like “Show: ψ”, where ψ is the statement we’d like to show using our existential assertion. We’ll then make an assumption of the form *φ*_{x}(*c*), where *c* is a fresh constant (in particular, *c* does not occur in ψ). The idea is that this *c* is the temporary name we’re giving to the thing whose existence we’re assured of by the statement ∃*x**ϕ*_{x}. We then go ahead and try reach the conclusion ψ. When we succeed, we need to cite three things:

- the line were we have ψ,
- the line where we have ∃
*x**ϕ*_{x}, and - the line where we assume
*ϕ*_{x}(*c*)

using the justification ED, for “existential derivation”

So, for example the argument ∃*x**F*(*x*),∀*x*(*F*(*x*)→*G*(*x*)) ⊢ ∃*x**G*(*x*) is valid, by the following derivation:

```
1. Show:ExG(x)
2. ExF(x):PR
3. Ax(F(x)->G(x)):PR
4. Show:ExG(x)
5. F(c):AS
6. F(c)->G(c):UI 3
7. G(c):MP 5 6
8. ExG(x):EG 7
9. :ED 2 8 5
10.:DD 4
```

### Problem Set 17

Please complete the following derivations: