10/13/26
Reading
Herrick[2000] The Many Worlds of Logic Chapter 18
The Tutorial
There is a rule for adding a Existential Quantifier. This permits the step illustrated by the following proof fragments.
5 Fa 6 (∃x)Fx 5 EG
5 Fb 6 (∃x)Fx 5 EG
5 Fb 6 (∃z)Fz 5 EG
To understand what this rule permits, it helps to think about it as though you were going backwards from line 6 to line 5. Take the scope of line 6, which is Fx, Fx, and Fz respectively, then substitute a term for free occurrences of the variable of quantification-- you should be able to get line 5, and indeed you can.
Sad to say, like Universal Instantiation and Generalization, there is a rather sophisticated restriction on this rule-- we will come to this in Tutorial 23.
The Simplified Rule of Existential Generalization EG
If a derivation contains a line of the form
n. <formula>[<term>/<variable>]> <any justification>
then a line of the form
(∃<variable>)<formula> 'n EG'
may be added to the derivation, provided that <variable> is new to <formula>.
Exercise to accompany Predicate Tutorial 10
Exercise 1 (of 1)
Derive the following
a) Fb∴(∃x)Fx
b) Fa∴(∃y)Fy
c) Fa∴(∃x)Fa
d) Fa,Ga∴(∃x)(Fx&Gx)
e) Fa,Ga∴(∃x)(Fx&Ga)
f) Fa,Ga∴(∃x)(Fa&Gx)
g) Fa,Ga∴(∃x)(Fx)&Ga