Barber Paradox Why is this model inconsistent?

Question

I would like to know why is this model inconsistent? We can have the following tuples in shaves.

shaves = {(man,man)} sig Man {shaves: set Man} one sig Barber extends Man {}

fact {
   Barber.shaves = (m:Man |m not in m.shaves}
}

Barber.shaves will produce 0 tuples. In this case, fact should be valid. So why does allow tell me that my model is inconsistent?

Would really appreciate some advice on this.

Answer 1

There is a simple explanation using only English.

The Alloy fact above says that the set of men that the barber (there is only one barber, since one sig Barber) shaves is exactly equal to all men who don't shave themselves. At first, this statement makes sense, because every man either shaves himself or is shaved by the barber.

The trick question is then "who shaves the barber". If the barber doesn't shave himself, then the fact forces that the barber must shave the barber, which is in contradiction with the assumption that the barber doesn't shave himself. If the barber does shave himself, then the fact forces that the barber must not shave the barber, which is again a paradox, so no instance can be found.

Answer 2

Okay here is the solution. The idea is really simple, and I think the authors really ought to explain this in their book.

The crux of the confusion is in the fact statement.

Barber.shaves = {m:Man | m not in m.shaves}

Basically, what the above statement is saying is that, any tuples in Barber.shaves must not shave himself. For example = Barber.shaves = {(m)}, then (m, m) MUST never occur in the shaves relations set. Also m:Man indicates that every man that does not shave himself should also be in Barber.shaves.

The problem occurs when we come to the Barber instance. If barber is not in Barber.shaves, then it violates m : Man. If barber is included, then it violates m not in m.shaves since shaves would contain {(barber, barber)}

I hope this clears up the confusion for beginners in alloy like myself.

So given the current model in my question, alloy cannot create an instance that satisfies this fact.