Demo A

Multiple Quantifier Demo

This simple derivation merely switches the order of quantifiers. Notice how
we deal with multiple quantifiers: *One at a time.*

Line 1 has main connective '%'. This usually
makes one think of setting up for %E.

But our assumption on line 2 also has main connective '%'.
So, we need to prepare %E once again! (%E
does *not* allow us to do the two necessary substitutions at once.)

The
filling in should now be obvious. We apply %I twice
to derive our preliminary goal...

Finally, we have the two ingredients needed as input for %E:
the existential statement *( green)
and* the appropriate subderivation (

We have to do this twice to make use of the two sentences with main connective '%'.

Notice
the assumption (line 2) and the new goal (line 6). The preliminary goal of
line 6 is of course the same as the ultimate goal. That's fairly typical for
%E.

Again
the last line of the subderivation is the same as the goal outside the subderivation.
That's just setting up so that we can apply %E twice
at the end when we have finished the two necessary subderivations.