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 (blue).
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.