The Revenge of Problem 3.f
				  by
			   Gary T. Leavens


			       Abstract

Kishore's proof of problem 3.f (Cohen's 2.1(i)) turns out to use a fallacy
in the crucial step.  Trying to repair this proof reveals an elegant proof
and a lemma with all the inelegant details.  This discussion reveals the
importance of being "very careful" and something about metamathematics.

1. Kishore Doobagunta's solution

Recall homework problem 3.f (Cohen's 2.1(i)) was to
	prove: (X ==> (Y equiv Z)) ==> (X /\ Y ==> Z).
I guess I started the difficulty with this by asking for elegant proofs.
Most of you had given proofs of this that were convincing, but consisted
in expanding out the implications using various laws, distributing,
and then using idempotence and "P equiv P" to reduce the whole thing to true.
I too had looked for more elegant proofs, without success.

So I was pleased when Kishore Doobagunta volunteered his fairly short proof,
which is reproduced below.  I have taken the liberty of writing it backwards,
and making a few other minor modifications.

      (X /\ Y) ==> Z
equiv	<Impl>
      (X /\ Y) \/ Z equiv Z
equiv	<Golden Rule>
      (X \/ Y equiv Y equiv X) \/ Z  equiv Z
equiv	<distribution of disjunction over equivalence>
      (X \/ Y equiv Y) \/ Z equiv X \/ Z  equiv Z
  <==	<by P \/ Q <== P with P:=(X \/ Y equiv Y), Q:=Z; call this step (*)>
      X \/ Y equiv Y equiv X \/ Z  equiv Z
equiv	<associativity and symmetry>
      X \/ Y equiv X \/ Z equiv Y equiv Z
equiv	<distribution of disjunction over equivalence>
      X \/ (Y equiv Z) equiv Y equiv Z
equiv	<Impl>
      X ==> (Y equiv Z)

There it is, a proof admirable for it's elegance and even it's symmetry.
In this order, there aren't even any rabbits jumping out of the hat.
(I don't consider it circular to use the consequence instead of the
implication, as you can think of the consequence as simply a notational
abbreviation.  If that bothers you, write it in the Kishore's order,
using implication instead of consequence.)

Unfortunately, the above proof is not valid!  I should have seen this in
class, but I was too carried away with the boldness of the step (*)
to think about whether the step could be invalid.  What does it mean
for this step to be valid?  Well, it's a step of the form:

	    C equiv B
	<==	<hint why C <== A>
	    A equiv B

or if you write the proof in the way Kishore wrote it originally,
it's a step of the form.

	    A equiv B
	==>	<hint why A ==> C>
	    C equiv B

I happened to read Cohen's chapter 6 again last night in preparing notes,
and Cohen points out that such a step means:

	(A ==> C) ==> ((A equiv B) ==> (C equiv B))

So the step marked (*) above is valid if and only if this is valid.
Is it?  (You might want to think about this yourself before reading on.)

2. The fallacy

It turns out that the formula 

	(A ==> C) ==> ((A equiv B) ==> (C equiv B))		(**)

is not valid.  There are probably many ways to show this.
What I tried to do was to prove it.  I started to calculate...

      (A equiv B) ==> (C equiv B)
equiv	<Impl>
      (A equiv B) \/ (C equiv B) equiv C equiv B
equiv	<distribution of disjunction over equivalence>
      (A equiv B) \/ C equiv (A equiv B) \/ B equiv C equiv B
equiv	<distribution of disjunction over equivalence>
      A \/ C equiv B \/ C equiv A \/ B equiv B \/ B equiv C equiv B
equiv	<idempotence of disjunction, associativity>
      A \/ C equiv C equiv B \/ C equiv A \/ B equiv B equiv B
equiv	<Impl, trying to connect to A ==> C>
      A ==> C equiv B \/ C equiv A \/ B equiv B equiv B
equiv	<P equiv P, true is unit of equivalence>
      A ==> C equiv B \/ C equiv A \/ B				(***)

At this point I haven't made any mistakes, but I don't know how to proceed.
So, and this is something you have to think about when you're trying to
prove something that may not be true, I started looking for a counterexample.
That is, I looked for values of A, B, and C such that formula (***)
above would be true, but (A ==> C) would be false; this would give
a counterexample to formula (**).  (See why?)  We can make (A ==> C) false
only by making A true and C false.  So we have:
	A = true,
	C = false.
What to choose for B?  Well, we have (A ==> C) = true now, so (***) will
be false if and only if ((B \/ C) equiv (A \/ B)) is false.
We know A is true, so (A \/ B) is true. (why?)  So we need to make (B \/ C)
false, but as C is false, we can do this with
	B = false.
This provides the counterexample.

In conclusion, Kishore's proof is, sadly, fallacious.
The fallacy is, in summary, that you can't substitute blindly if you
don't have equality (or equivalence, which is equality for booleans).

At this point you might want to try to construct an elegant proof of
the original problem (3.f).  But be warned, it's not easy.

3. A better proof

After finding that the step Kishore took was fallacious, I tried to repair
his proof.  It turns out not to be easy to do.  But I did take from Kishore's
proof two ideas that helped find an elegant proof:
	- it would be nice to use implication (or consequence)
		as a connective between steps, and
	- I might try to keep implications in the proof longer,
		instead of getting rid of them.
Because I was thinking about keeping implications in the proof,
I tried using the rule of mutual implication.  This lead to the following
proof.

      X ==> (Y equiv Z)
equiv	<Mutual implication>
      X ==> ((Y ==> Z) /\ (Z ==> Y))
==>	<Now I want to just drop the (Z ==> Y), as in Kishore's proof.
		I can do this if (X ==> (A /\ B)) ==> (X ==> A) is valid;
		it is, but I'll make that a lemma, which I cite here.>
      X ==> (Y ==> Z)
equiv	<by exercise 2.1(e)>
      X /\ Y ==> Z

Now that's a short proof, and very elegant.  At least I think it
clearly conveys the idea of the proof.
The only trouble is that I now have to show the lemma.

Lemma: (X ==> (A /\ B)) ==> (X ==> A)

The interesting thing is that all the inelegance hasn't gone away,
it's gone into the lemma!  And there's a very good (metamathematical)
reason for that: the lemma is about throwing away information about B.
The only rule we have, at this point in Cohen's book, that throws away
information is:
	P equiv P equiv true.
That allows us to say that if we have (P equiv P),
then we can throw it all away and get true
(which in a sense has no information).  So the only strategy
here is to expand everything and then apply (P equiv P);
but at least, by this metamathematical argument, I don't have to feel
guilty about having an inelegant proof.

Proof:

      (X ==> (A /\ B)) ==> (X ==> A)
equiv	<Impl>
      (X ==> (A /\ B)) \/ (X ==> A) equiv X ==> A
equiv	<the conjunction will cause problems in distribution,
		so to eliminate I use the Golden Rule>
      (X ==> (A \/ B equiv A equiv B)) \/ (X ==> A) equiv X ==> A
equiv	<towards distributing, use Impl>
      ((X \/ (A \/ B equiv A equiv B) equiv (A \/ B equiv A equiv B))
       \/ (X ==> A))
      equiv X ==> A
equiv	<distribution of disjunction over equiv>
      ((X \/ A \/ B equiv X \/ A equiv X \/ B equiv A \/ B equiv A equiv B)
       \/ (X ==> A))
      equiv X ==> A
equiv	<again towards distributing, use Impl,
		and towards P equiv P, use Impl on the other implication>
      ((X \/ A \/ B equiv X \/ A equiv X \/ B equiv A \/ B equiv A equiv B)
       \/ (X \/ A equiv A)
      equiv X \/ A equiv A
equiv	<distributing disjunction over equiv>
      (X \/ A \/ B) \/ (X \/ A equiv A)
      equiv (X \/ A) \/ (X \/ A equiv A)
      equiv (X \/ B) \/ (X \/ A equiv A)
      equiv (A \/ B) \/ (X \/ A equiv A)
      equiv A \/ (X \/ A equiv A)
      equiv B \/ (X \/ A equiv A)
      equiv X \/ A equiv A
equiv	<distributing disjunction over equiv, using parenthesization above,
		and idempotence of disjunction to avoid listing duplicates,
		and symmetry of disjunction to list in order X, A, B>
      X \/ A \/ B equiv X \/ A \/ B
      equiv X \/ A equiv X \/ A
      equiv X \/ A \/ B equiv X \/ A \/ B
      equiv X \/ A \/ B equiv A \/ B
      equiv X \/ A equiv A
      equiv X \/ A \/ B equiv A \/ B
      equiv X \/ A equiv A
equiv	<associativity>
            X \/ A \/ B equiv X \/ A \/ B equiv X \/ A \/ B
      equiv X \/ A equiv X \/ A equiv A \/ B equiv A
      equiv
            X \/ A \/ B equiv X \/ A \/ B equiv X \/ A \/ B
      equiv X \/ A equiv X \/ A equiv A \/ B equiv A
equiv	<note that the above formula has two identical halves, so by P equiv P>
      true

One way to do the last two steps, is to just count the formulas of each shape
that appear in the 3rd formula from the end.  If there are an even number
of each shape, then P equiv P applies immediately.

4. Some conclusions

This problem illustrates several important issues.

The first is that sometimes there are good reasons to work proofs by
a brute force expansion and contraction.  But it is good to think at the
level of metamathematics (i.e., about the proof) to know why, and when
to stop looking for a proof that is more elegant (for the lemma).
Thus sometimes such metamathematics can help guide your proof process,
if you consciously step back and try to find reasons for trouble when
trouble happens.  (Of course, this is something that will become
easier when you see more examples of it.)

Another thing I think we can conclude is the value of using lemmas.
The proof of the lemma, while complex, is not as complex as
the proof of all of 3.f done in the style of the lemma.
This is because in the lemma, we use simple variables, A and B,
instead of manipulating more complex stuff from the original problem.
Furthermore, now that we have proved the lemma, we can use it again,
without going through the same pain.
But the most compelling reason is that now the proof of 3.f makes some
sense, and tells us something about the formula we are proving.
For me, that will help me remember the formula we proved, and the lemma.

Another conclusion is that by knowing what a calculation means, we can
check the validity of the steps in a proof.  This allows us to check dubious
steps, as we did to find the fallacy above.

Another conclusion is that it's often interesting to examine solutions
to see how or whether they can be improved.

Finally, about time and the revenge referred to in the title.
I'm sure a lot of you spent a long time working on problem 3.f.
But I think it turned out to be a highly interesting problem.
And the problem has exacted your revenge on me, as I've now spent about
twelve hours on it.  But I learned some things, and it's been fun.
This reminds me of the following poem by Piet Hein.

		PROBLEMS

		Problems worthy
		  of attack
		prove their worth
	          by hitting back.


      (X /\ Y) ==> Z
equiv	<Impl>
      (X /\ Y) \/ Z equiv Z
equiv	<Golden Rule>
      (X \/ Y equiv Y equiv X) \/ Z  equiv Z
equiv	<towards applying the rule P \/ Q <== P, disjunction is idempotent>
      (X \/ Y equiv Y equiv X) \/ Z  equiv Z \/ Z
equiv	<distribution of disjunction over equivalence>
      (X \/ Y equiv Y equiv X equiv Z) \/ Z
  <==	<by P \/ Q <== P; call this step (*)>
      X \/ Y equiv Y equiv X  equiv Z

      X \/ Y equiv Y equiv X \/ Z equiv Z
equiv	<associativity and symmetry>
      X \/ Y equiv X \/ Z equiv Y equiv Z
equiv	<distribution of disjunction over equivalence>
      X \/ (Y equiv Z) equiv Y equiv Z
equiv	<Impl>
      X ==> (Y equiv Z)