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
  1. Universal Instantiation (abbreviated UI), the argument form

xϕx ⊢ ϕx(c)

is a rule of direct inference

  1. 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:

exercise 16.1
16.1 Ax(F(x)/\G(x)) :|-: F(c)
exercise 16.2
16.2 Ax(F(x)), F(c) -> G(c) :|-: G(c)
exercise 16.3
16.3 Ax(F(x)), F(b)/\F(c) -> G(c) :|-: ExG(x)
exercise 16.4
16.4 AxAy(F(x) -> G(y)), F(c) :|-: G(d)
exercise 16.5
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 ⊢∀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)) ⊢ ∀xF(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:

exercise 17.1
17.1 Ax(F(x)->G(x)), AxF(x) :|-: AxG(x)
exercise 17.2
17.2 Ax(F(x)->G(x)), Ax(G(x)->H(x)) :|-: Ax(F(x)->H(x))
exercise 17.3
17.3 Ax(G(x)/\G(c)) :|-: AxG(x)
exercise 17.4
17.4 Ax-F(x), F(d) :|-: -AxF(x)
exercise 17.5
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 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:

  1. the line were we have ψ,
  2. the line where we have xϕx, and
  3. the line where we assume ϕx(c)

using the justification ED, for “existential derivation”

So, for example the argument xF(x),∀x(F(x)→G(x)) ⊢ ∃xG(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:

exercise 17.6
17.6 Ex(F(x)/\G(a)) :|-: G(a)
exercise 17.7
17.7 Ax(F(x)->G(x)), ExF(x) :|-: ExG(x)
exercise 17.8
17.8 Ax(F(x)->G(x)), Ex(F(x)/\H(x)) :|-: Ex(G(x)/\H(x))
exercise 17.9
17.9 Ax(F(x)->G(x)), -Ex(F(x)/\G(x)) :|-: -ExF(x)
exercise 17.10
17.10 Ex-F(x) :|-: -AxF(x)