Сплав - решение парадокса Барбера все еще противоречиво

Question

Известно, что парадокс парикмахера решается, если есть несколько парикмахеров, чтобы они могли брить друг друга.

Эта спецификация соответствует:

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

Тем не менее, следующее, хотя это выглядит эквивалентно, все еще противоречиво:

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

Зачем?

Answer 1

В первом факте вы ограничиваете: то, что множество людей, выбритых всеми парикмахерами, - это все люди, которые не бреются сами.

Редактировать мое объяснение второго факта наверняка не хватило ясности. Вы утверждаете, что человек считается парикмахером, если набор людей, которых он бреет, равен набору всех людей, которые не бреют себя (включая его, именно отсюда и непоследовательность, и в этом вся прелесть этой проблемы).