How to solve the liar problem?

Question

In an island live two kinds of people: liar and truth-teller, the former only tells lies and the latter only tells truth, now there're two men A and B from the island, A said: "B is a truth-teller." B said: "We two are different kinds of people." Please identify the sort of them.

If we mark A with a and B with b and use True to represent truth-teller, the answer is apparently b == False && a == False . This seems to be easy to translate into mathematica code, I first tried:

Reduce[{Refine[a, b == True] == False, Refine[b, a == True] == True}]
(* b == True && a == False *)

…What's this? Maybe I have some misunderstandings for the Functions… I didn't think much and tried another approach:

Reduce[{Implies[b == True, a == ! b], Implies[a == True, b == True]}, {a, b}]
(* (a == False && b == True) || (a - True) (-b + True) != 0 *)

…What's this? Maybe I have some misunderstandings for the Functions… I didn't think much and tried my third approach:

Reduce[{If[b == True, a == ! b, a == b], If[a == True, b == True, b == False]}]
(*b == False && a == False && False - True != 0*)

…This time I get the right answer, but what's False - True != 0!? Reduce doesn't know booleans?

Surely I'm not solving the problem in the right way, how to get the answer properly with mma? And I would be appreciate if you can tell me where I'm wrong in the first two samples.

---

…I forgot a important thing: in logic, if $p$ is false and $q$ is true, then $p\Rightarrow q$ is still true, so my first two translations for the liar problem is incomplete and the third one is correct because I unconsciously add the missing rule in If, so my second sample should be modified to:

Reduce[Implies[b == True, a == ! b] && 
       Implies[b == False, a == b] && 
       Implies[a == True, b == True] && 
       Implies[a == False, b == False], {a, b}]
(* 
   (a == False && b == False && False - True != 0) || 
   (a - False) (-b + False) (a - True) (b - True) != 0 
 *)

Though the result is still a little strange, at least this time the right answer is involved in it, and together with the comment from @Daniel Lichtblau it's not that unacceptable now.

And of course the answer from @halirutan using !Xor is terser.

And had I noticed the correct syntax for SatisfiabilityInstances earlier, perhaps I would have lost my curiosity and this question wouldn't exist anymore…:

SatisfiabilityInstances[Implies[b == True, a == ! b] && 
                        Implies[b == False, a == b] && 
                        Implies[a == True, b == True] && 
                        Implies[a == False, b == False], {a, b}]
(* {{False, False}} *)

SatisfiabilityInstances[If[b == True, a == ! b, a == b] && 
                        If[a == True, b == True, b == False], {a, b}]
(* {{False, False}} *)

However, I'm still unable to give a good explanation for my first sample: as we've seen, it gives an answer similar to the second sample, but:

SatisfiabilityInstances[Refine[a, b == True] == ! b && 
                        Refine[a, b == False] == b && 
                        Refine[b, a == True] == True && 
                        Refine[b, a == False] == False, {a, b}] 
(* {} *)

…Why?

---

…I get the truth: Refine is not available for the logical judgement，and the "right" answer for the first sample is just a illusion, that's just because a and b don't have a explicit relationship so the assumption inside Refine is considered as something meaningless by Reduce, the process is similar to:

Reduce[{Refine[a, b == 3] == 1, Refine[b, a == 4] == 2}]
(* b == 2 && a == 1 *)

OK, now it's all clear 囧.

Answer 1

Have you seen, that Mathematica is capable of many boolean computations using special boolean functions? Let's assume someone from the island makes a statement, then when the statement is true, whether or not he tells the statement is true, depends on whether or not he is a truth-teller. When we know, which kind he is, we know the correct statement through what he says. Therefore, let's define a function for this and check the truth-table

trueStatement[statement_,isTruthTeller_]:=!Xor[statement,isTruthTeller]    
BooleanTable[{a,b,trueStatement[a,b]},{a,b}]//TableForm
(*
True    True    True
True    False   False
False   True    False
False   False   True
*)

So, if A says a statement is true and A is a truth-teller, the statement is true for sure. On the other hand, if A is not a truth-teller, then the real statement is false.

Now we want to transform the two statements

A said: "B is a truth-teller." B said: "We two are different kinds of people."

without knowing whether a or b are liars or truth-tellers

eq = trueStatement[b, a] && trueStatement[a == ! b, b]

The statements read as: a says that b is a truth-teller and b says, that a is not of the same kind as b. Now we can simply do

SatisfiabilityInstances[eq, {a, b}]

(* {{False, False}} *)

Therefore, both, a and b are liars.

Answer 2

Cases[Tuples[{True, False}, 2], {a_, b_} /; 
  Equivalent[a, b] && Equivalent[b, Xor[a, b]]]

(*{{False, False}}*)

FindInstance[Equivalent[a, b] && Equivalent[b, Xor[a, b]], {a, b}, Booleans]

(*{{a -> False, b -> False}}*)

Answer 3

Proposition a : A is a truth - teller,

Proposition b : B is a truth - teller

A said : "B is a truth-teller." We observe: a True iff b True

Hence :

a [Equivalent] b is a tautology.

B said : "We two are different kinds of people."

We observe b True iff the above proposition is True .

Hence :

b [Equivalent] (a [Xor] b) is a tautology.

Solution :

FindInstance[{a [Equivalent] b, b [Equivalent] (a [Xor] b) }, {a, b}, Booleans ]

{{a -> False, b -> False}}

Conclusion: Both A and B are liars.