Multiple Quantifier Demo
This simple derivation merely switches the order of quantifiers. Notice how
we deal with multiple quantifiers: One at a time.
Start the demonstration...
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.)
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
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
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.