Proof by using multiple theorems

Hi all,

I have the solution to this question, but i don't understand how it was derived. And i hope someone could further explain it to me. A lot of theorems have been used such as modus tollen, proof by contradiction, etc.

Qns:

Knights always tell the truth, knaves always lie.

Can we tell what A and B are, from what they say below?

A: B is a knight

B: A and I are of opposite type.

Let a = "A is a knight"

Let b = "B is a knight"

Solution:

- a
- therefore b -- A tells the truth
- therefore (a^~b) v (~a^b) -- B tells the truth (**)
- therefore a^~b -- elimination
- therefore ~b -- specialization
- therefore c (contradiction)
- therefore ~a -- by contradiction
- ~b -- A lies

The above argument tells us that if there is a solution, it must be that both A and B are knaves.

My question:

From (**) onwards, i start to not understand the solution. Firstly, how do we know which we should eliminate at 3? When specializing at 5, why can't we select "a" instead of "~b". Do i just select anyone? And how does it lead to "c" from "~b" at 5 to 6?

Thanks for your help in advance!