床屋のパラドックス

集合論が提唱された当初、任意の述語 P に対して P を満たす要素の集合 { x | P x } が存在するとされていました。このルールを内包公理と呼びます。P が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 P として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。

この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。

以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。

その内容は自然言語では次のように説明できます。

この内容を Lean で表現してみましょう。演習問題として、sorry の部分を埋めてみてください。

namespace Barber

/-- 全体集合となる人々の集合 -/
opaque Person : Type

/-- p さんが q さんの髭を剃るという述語 -/
opaque shave (p q : Person) : Prop

-- 床屋が存在するという仮定
variable (barber : Person)

-- 床屋の信念を仮定として表現したもの
variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p)

example : False := by
  sorry

end Barber