Tutorial 21: Existential Instantiation, and Quantifier Replacement Rules

Logical System

2/5/08 10Software

Reading

Hausman[2007] Logic and Philosophy Chapter 9

The Tutorial

Existential Instantiation permits you to remove an existential quantifier from a formula which has an existential quantifier as its main connective.

The circumstance that Existential Instantiation gets invoked looks like this.

  (∃x)<scope> ?
  ? ? <<

For example,

  (∃x)Fx ?
  ? ? <<

It is easy to get a rough sense of what this should permit. (∃x)Fx says that 'something is F ' so what it should permit is an inference to, say, Fa ie 'a is F', where 'a' is the name of that thing which is F.

However, setting this up properly gets awkward at this point. Any rules we have should permit only valid inferences. Consider the following three inferences

(∃x)Fx ∴ Fa
(∃x)Fx ∴ Fx
(∃x)Fx ∴ Fy

The first, which uses an inference to a constant, is not valid, because it does not follow from 'Something is F' that 'a is F' because the thing that is F might be b, or c, or something else. [From 'Something is fat' it does not follow that 'Arthur is fat' for it could be Bill or Charlie that are the fat ones.]

The second and third, which use inferences to variables, are not valid either, because x or y in the conclusions are free variables and there could be interpretations and valuations in which the premise is true (say with Arthur being fat) yet the conclusion false (with x or y being valued to Bill or Charlie, say).

We seem to be stuck. Apparently there are two ways forward. We could go with an inference to a constant like (∃x)Fx ∴ Fa but understand the 'a' here not as the pre-assigned name of Arthur but rather as as arbitrary floating name of whatever thing it is that is F. Or we could go with an inference to a variable like (∃x)Fx ∴ Fy but understand the 'y' here not as an ordinary free variable but rather as the definite name of something (which does not need a valuation in the semantics), a kind of an unknown name, a quasi variable name.

In the Hausman book, the second choice is made

Yet more care has to be taken here because the variable 'y' may already be in the proof and, in fact, we may be able to prove Gy-- in which case we may be tempted to think that (∃x)Fx and Gy can give us (Fy and Gy) which it should not because there is no assurance that the thing which is F is the same thing as the thing which is G. What is needed here is that the 'y' or, to give it another description, the instantiating quasivariable, be new to the proof.

The resulting rule permits any of the following

n (∃x)Fx ?
  Fw n EI

 

n (∃x)Fx ?
  Fy n EI

 

provided 'w' and 'y' etc are new to their respective proofs.

Quantifier Replacement Rules

With the sentential logic, it was useful to have some replacement or rewrite rules, like De Morgan's Law, to shorten some of the derivations. The same is true for predicate logic, and a couple of useful rules involve the interaction of the quantifiers with negation.

In English, 'Not all...' is equivalent to 'There is ... not...'; for example, 'Not all dwarves are happy' is equivalent to 'There is a dwarf who is not happy'. Similarly 'Not exists...' is equivalent to 'All ... not...'; for example, 'There does not exist a dwarf who is happy' is equivalent to 'All dwarves are not happy'.

These equivalences are enshrined as replacement rules (available off the Replacement Rules menu).

~(m)p::(∃m)~p
(m)~p::~(∃m)p

(where m is a pattern for a variable and p is a pattern for a well formed formula).


Exercise to accompany Predicate Tutorial 11.

Exercise 1 (of 2)

Proofs


Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

Derive the following

a) (∃x)(Fa) ∴ Fa /*a little bit of a trick, this one*/

b) (∃x) (Fx.Gx) ∴ (∃x)(Fx )

c) (∃x) (Fx.Gx) ∴ (∃y)(Gy)

d) (∃x)(Fx)∴ (∃y)(Fy)

e) (∃x)(Fx.Gx) ∴ (∃y)(Fy).(∃z)(Gz)

Exercise 2 (of 2)

Proofs


Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

Each of following derivations will use Existential Instantiation at some stage.

Derive

a) ∴ (∃x)Fx≡(∃y)Fy

b) (x)Fx,(∃x)~Fx∴G

c) ∴ (∃x) (Fx∨Gx) ≡ (∃y)Fy∨(∃z)Gz

d) (∃x)(Fx∨Gx),(x)(Fx⊃Hx),(x)(Gx⊃Hx)∴(∃x)Hx

e) ~(∃x)(Fx.~Gx),~(∃x)(Gx.~Hx)∴(x)(Fx⊃Hx)

f) ~(∃x)Gx,(x)(Fx⊃Gx)∴(x)(Fx⊃Hx)

g) (∃x)Fx∨(∃x)Gx,(x)((Fx∨Gx)⊃Hx)∴(∃x)Hx