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:
  1. a
  2. therefore b -- A tells the truth
  3. therefore (a^~b) v (~a^b) -- B tells the truth (**)
  4. therefore a^~b -- elimination
  5. therefore ~b -- specialization
  6. therefore c (contradiction)
  7. therefore ~a -- by contradiction
  8. ~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!