8/11/2026
The Tutorial
There is a rule for adding a Existential Quantifier. This permits the step illustrated by the following proof fragments.
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, 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
Should you wish to use the Deriver application, see Exercises for Easy Deriver using the Deriver Web Application [Gentzen] . Good advice is: start these tutorials without out it, but if you get to the point of wishing to save some work, then switch to the Deriver Web Application.