#Chapter 12: 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 $\phi$ and $\psi$ that lets us pay special attention to variables.
So, we allow for the following convention. $\phi_x$ is a sentence where we are
paying special attention to the free (not bound by any quantifier in $\phi_x$)
occurrences of the variable $x$. $\phi_x(c)$ is a sentence where we have
replaced every free occurrence of the variable $x$ with an occurrence of a
constant $c$. So, $\phi_x$ might contain some occurrences of $c$. But
$\phi_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

:   1. *Universal Instantiation* (abbreviated UI), the argument form

       $\forall x \phi_x \vdash \phi_x(c)$

       is a rule of direct inference

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

       $\phi_x(c) \vdash \exists x \phi_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:

```{.ProofChecker .FirstOrder}
16.1 Ax(F(x)/\G(x)) :|-: F(c)
16.2 Ax(F(x)), F(c) -> G(c) :|-: G(c)
16.3 Ax(F(x)), F(b)/\F(c) -> G(c) :|-: ExG(x)
16.4 AxAy(F(x) -> G(y)), F(c) :|-: G(d)
16.5 AxAy(F(x) <-> G(y)), F(c) :|-: F(d)
```

##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 $\vdash\forall 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 $\forall x(F(x)\land G(x))\vdash\forall x F(x)$.

``` 
1. Show: AxF(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:

```{.ProofChecker .FirstOrder}
17.1 Ax(F(x)->G(x)), AxF(x) :|-: AxG(x)
17.2 Ax(F(x)->G(x)), Ax(G(x)->H(x)) :|-: Ax(F(x)->H(x))
17.3 Ax(G(x)/\G(c)) :|-: AxG(x)
17.4 Ax-F(x), F(d) :|-: -AxF(x)
17.5 -ExF(x) :|-: Ax-F(x)
```

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 $\exists x
\phi_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 $\exists x\phi_x$. We then go ahead and try reach the conclusion
ψ. When we succeed, we need to cite three things:

1. the line were we have ψ,
2. the line where we have $\exists x \phi_x$, and
3. the line where we assume $\phi_x (c)$

using the justification ED, for "existential derivation"

So, for example the argument $\exists xF(x), \forall x(F(x)\rightarrow
G(x))\vdash \exists 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:

```{.ProofChecker .FirstOrder}
17.6 Ex(F(x)/\G(a)) :|-: G(a)
17.7 Ax(F(x)->G(x)), ExF(x) :|-: ExG(x)
17.8 Ax(F(x)->G(x)), Ex(F(x)/\H(x)) :|-: Ex(G(x)/\H(x))
17.9 Ax(F(x)->G(x)), -Ex(F(x)/\G(x)) :|-: -ExF(x)
17.10 Ex-F(x) :|-: -AxF(x)
```
