理髮師悖論爲什麼這個模型不一致？

Question

我想知道爲什麼這個模型不一致？我們可以在剃鬚刀中使用下列元組。

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將產生0的元組。在這種情況下，事實應該是有效的。那麼爲什麼允許告訴我，我的模型是不一致的？

真的很感激這方面的一些建議。

Answer 1

有一個簡單的解釋，只使用英語。

上面的合金事實表明，理髮師（只有一個理髮師，因爲one sig Barber）刮鬍子的那一套男人是完全等於所有不刮鬍子的男人。起初，這種說法是有道理的，因爲每個人不是剃自己就是被理髮師剃光。

那麼詭計的問題是「誰刮理髮師」。如果理髮師不剃自己，那麼這個事實迫使理髮師必須剃理髮師，這與理髮師不剃自己的假設相矛盾。如果理髮師自己刮鬍子，那麼這個事實迫使理髮師不能剃理髮師，這又是一個悖論，所以沒有任何事例可以找到。

Answer 2

好的，這裏是解決方案。這個想法非常簡單，我認爲作者真的應該在他們的書中解釋這一點。

混淆的癥結在於事實陳述。

Barber.shaves = {m：Man |在m.shaves}

基本上不中號，上面有哪些說法是說的是，在Barber.shaves任何元組不能刮鬍子自己。例如= Barber.shaves = {（m）}，那麼（m，m）必須在剃鬚關係組中不會出現。另外男：男人表示，每個不剃自己的男人也應該在Barber.shaves。

當我們來到理髮師實例時會出現問題。如果理髮師不在Barber.shaves，那麼它違反了m：Man。如果包括理髮師，那麼它會違反m而不是m.shaves，因爲剃鬚膏會含有{（理髮師，理髮師）}

我希望這能夠解決像我這樣的合金初學者的困惑。

所以，鑑於當前模型，我的問題，合金不能創建一個實例，它滿足了這一事實。