Alloy - solution to Barber paradox still inconsistent

323 Views Asked by At

It is known that the barber paradox is solved if there are multiple barbers so that they can shave each other.

This specification is consistent:

 sig Man {shaves: set Man} 
 some sig Barber extends Man {} 
 fact {   
   Barber.shaves = {m: Man | m not in m.shaves} 
 } 
 run { } for 4

However, the following, albeit it looks equivalent, is still inconsistent:

sig Man {
 shavedMen : set Man
}
fact {
 # {barber:Man | barber.shavedMen = {m: Man | m not in m.shavedMen} } > 1
}
run {} for 4

Why?

1

There are 1 best solutions below

2
On

In the first fact you constrain: that the set of man shaved by all barbers are all the men that do not shave themselves

Edit my explanation of the second fact certainly lacked of clarity. You state that a man is considered barber if the set of man he shaves is equal to the set of all men that do not shave themselves (him included, that's where the inconsistency comes from, and that's all the fun of this problem).