The Love Reciprocated Demo
Suppose that everyone loves someone (that is, '(^x)(%y)Lxy'
is true on one obvious interpretation of 'L'). And that if one person loves
a second, that love is reciprocated ('(^x)(^y)(Lxy>Lyx)').
Too ideal, of course! But given these two premises, it follows that everyone
is loved by someone. ('(^x)(%y)Lyx'; note
that 'y' and 'x' have been swapped from their positions in the first premise.)
First, see if you can make sense of the above, then do the derivation...or
perhaps you should do the derivation first, then see if you can comprehend
the first paragraph above!
Start the demonstration...
think ahead: this derivation should end by ^I. This
requires a substitution instance (of 10) at line 9.
1 and ^E should help...1 looks so much
like our goal. The two simply have the order of the L-relationship between
x and y reversed.
As soon as you use this, you have a new existential sentence and
so need to prepare for %E. Make the usual (and appropriate)
assumption: pick a new name ('t' is ok) to illustrate the person loved by "a".
This gives a new preliminary goal within the subderivation
work on line 2. Both its universal quantifiers need to be eliminated. This
takes two steps (lines 5 and 6)!
do the obvious and then note that we have the two ingredients needed as input
for %E: the existential statement on line 3 (green)
and the appropriate subderivation (blue).
have derived (%y)Lya at line 9. But 'a' is arbitrary.
So, finish the derivation by using ^I.