2009-09-15 [長年日記]
λ. 推移閉包が一階述語論理で表現できないことの証明
推移閉包が一階述語論理で表現できないことについて何度か書いたけど、最近になって“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders)で、どうやって証明するかを知った。
二項関係 T が二項関係 R の推移閉包であることを論理式 φ によって表現できると仮定して、矛盾を導く。まず、
- σ0 = ￢R(a,b)
- σn+1 = ∀x1,…,xn+1. ￢(R(a,x1)∧R(x1,x2)∧…∧R(xn, xn+1)∧R(xn+1,b))
- Σ = {σn | n∈N }
- Γ = {φ, T(a,b)}∪Σ
と定義する。 すると、 Γ の任意の有限集合 Γ' は( σn∈Γ' であるような任意の n よりも2以上長いパスによって)充足可能なので、コンパクト性定理により Γ も充足可能なことが言える。 しかし、実際には Σ 全体は a から b へ到達不能であることを主張しているので、 Γ は充足出来ない。 これは矛盾なので、背理法よりこのような論理式 φ は存在しない。
コンパクト性定理って、あまり応用を知らなかったけど、こういう使いでがあるのね。便利だ。
関連
[ツッコミを入れる]
