In the final exam of ILO they were asking , and I needed a very very long time until I got it:
Remark that the result we're searching, , is a disjunction. Since you already know the disjunction introduction, you could simply search , and then use that rule to get . Or if with didn't work, you could try with , since if is true, then also is, and we're done.
Unfortunately, is not always true, and also isn't always true (on the other hand, is always true, and that's what we're trying to prove). After seeing this, we must search another method which works with the two formulas, and , at the same time, since it seems that if we take only one without looking at the other, then it does not provide much information.
To use the we must use proof by cases. We will try to see that both and lead to , since if we can do that, we will have finished.
implies , and if is true then also is, so implies .
With , what we know doesn't relate it to but to . We want . Hardly we will make true because of , so we will try to make true just the . To do so, we will use reduction to the absurd: suppose that is false, then it holds that thanks to the formula on line 3. But we were under the supposition that was true, so our hypothesis can't be true, thus is true, and so is .
Since is true, and both paths lead to , we finally see that is always true.
If you are skilled working with logical formulas, you will have seen that is . This simplifies the problem and helps understanding it faster. But anyway, you can't change to directly, you would have to do it step by step.
Daniel Clemente Laboreo 2005-05-17