Things get harder. Here's the solution to :

But first: here we will only use the two rules that help adding and removing implications, since it's the only operator appearing in the formulas.

We want , so we will have to do a hypothesis inside of which we should prove that . We now do that to simplify the problem: we open a subdemonstration at line 2. We won't close it until we discover that is true.

Now the problem is somehow easier. We just need to prove , and we have two lines with two truths: the first says that , and the second says that .

How can we achieve the ? Well, as always: we must suppose , and achieve that is true, in some way. Even if it doesn't seem very simple, it's what must be done, since implication introduction works that way. So we're going to open another hypothesis, now supposing , and let's see if we achieve . This will be a hypothesis inside a hypothesis, but there's no problem in doing that.

After writing line 3, and being inside a subsubdemonstration, we have available that , that , and that . We must prove . Now it isn't that hard, is it? If we know that , we can use implication elimination on line 1, and we will get the true formula . Since is also true (line 2), we can apply that rule again to discover that .

We then see that supposing leads us to the conclusion , so we can write down , which is what we wanted. Now we've gone outside the subsubdemonstration, and we're only under the supposition that is true. As we now see that this supposition implies the truth of the formula , we can end this subdemonstration concluding that .

is precisely what had to be proven, so we're finished.

Daniel Clemente Laboreo 2005-05-17