2006-03-30 [長年日記]
λ. 素敵な定理 ∀x∀y∃R (x R y)
<URL:http://d.hatena.ne.jp/nuc/20050504/p3> より。
集合論で証明出来るのはもちろんだが、ここでは集合論はあまり本質的ではないように思う。一階述語論理では関係を量化出来ないので、関係を集合にエンコードして量化する必要があった。しかし、高階述語論理*1ならば関係を量化出来るので集合論に頼る必要はなく、あとは単に R = λa.λb. T とおけばこの定理は直ちに言える。また、R = λa.λb. (a=x)∧(b=y) とおけば最初の集合論での構成に対応したものになる。
*1 ここでは二階述語論理で十分
[ツッコミを入れる]
