日々の流転

λ. Smullyan's drinkers' paradox を Alloy で

Paradoxes of classical predicate calculus - ヒビルテ (2007-08-28) で Smullyan's drinkers' paradox を扱った。

これは英語で書くと「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」で、論理式で書くと「∃p. (drink(p) → ∀y. drink(y))」というもの。 古典一階述語論理での演算子の意味を考えれば、当たり前ではある*1のだけど一見するとパラドクスに思えてしまう。

こないだは Agda で証明したので、今度は Alloy でも試してみる。

-- 個体領域
sig Person { }
fact { #Person > 0 } -- 個体領域は空ではない

-- 述語
one sig Drinkers { ext : set Person }
pred drink(p : Person) { 
  p in Drinkers.ext
}

-- test
pred show() { }
run show for 10 Person

-- Smullyan's drinkers' paradox
assert paradox {
  some x : Person | drink[x] implies (all y : Person | drink[y])
}
check paradox for 10 Person

これを Alloy Analyzer でチェックしてあげると、ちゃんと「No counterexample found」となる。 また、ここで「fact { #Person > 0 }」を削除すると、ちゃんとPersonが一人もいない例が反例として得られる。

2010-12-23 追記

上の書き方はあまり良くなかった。

• 空でないことは、濃度演算子を使うより、someを使って表現したほうが良い。
• 部分集合はDrinkersのようなシグネチャのフィールドにしなくとも、部分集合シグネチャを使えばより直接的に表現できる。

直すと以下のようになる。

-- 個体領域
sig Person { }
fact { some Person } -- 個体領域は空ではない

-- 述語
sig Drinker in Person { }
pred drink(p : Person) { 
  p in Drinker
}