Demo B:
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...

 

Replay the demonstration.
Next demo...

First 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

Next, work on line 2. Both its universal quantifiers need to be eliminated. This takes two steps (lines 5 and 6)!

Finally, 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).

We have derived (%y)Lya at line 9. But 'a' is arbitrary. So, finish the derivation by using ^I.