Proof by using multiple theorems
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.
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"
- 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.
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!