A group of three people, each of which is a liar (lies all the time) or is a truar (tells the truth all the time) are talking. B says that C and D are the same type (both liars or both truars). Someone then asks D, ``Are B and C the same type?'' What does D answer?
Here's our solution. Let b stand for "B" is a truar", and similarly for c and d. The statement ``C and D are the same type'' is formalized as c == d. Since B said it, we have b == (c == d). D's answer can be formalized as b ? c, where ? is either == if D answers ``yes'' or /== if D answers ``no'', and we have to determine which it is. Since D answers, we write this as d == (b ? c).
We manipulate d == b ? c under the truth of b == c == d. In the manipulation,we omit all parentheses because == is associative and == and /== are mutually associative.
d == b ? c --Fact
= < Fact b == c == d >
b == c == b ? c
By inference rule Equanimity, the last line is a theorem. But the last line is a theorem only if ? is ==. Therefore, we conclude that D answered ``yes''.