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''.