日々の流転

λ. ビジネス実務マナー技能検定試験2級

合格していた。

λ. Paradoxes of classical predicate calculus

The Coq Proof Assistant - A Tutorial の「Paradoxes of classical predicate calculus」のところが面白い。古典一階述語論理だと Smullyan's drinkers' paradox 「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」が証明できてしまうそうだ。 へぇ。

例によってagdaで示してみる。

drinker (!D::Set) (!d::D)
        (!EM::(X::Set) -> Either X (Not X))
        (!P::D->Set)
    :: Exist (\(x::D)-> P x -> (y::D) -> P y)
drinker =
    case EM (Exist (\(x::D) -> Not (P x))) of
      (Left e  )->
          struct
            fst :: D
            fst = e.fst
            snd :: P fst -> (y::D) -> P y
            snd = \(px::P fst) -> case e.snd px of { }
      (Right ne)->
          let f (!x::D) :: P x
              f = case EM (P x) of
                    (Left px  )-> px
                    (Right npx)->
                        let e :: Exist (\(x::D) -> Not (P x))
                            e  = struct
                                   fst :: D
                                   fst = x
                                   snd :: Not (P fst)
                                   snd = npx
                        in case ne e of { }
          in struct
               fst :: D
               fst = d
               snd :: P fst -> (y::D) -> P y
               snd = \(z::P d) -> f

ところで、zyxwvさんが謎と思っているのはどの部分なんだろう?　一階述語論理の推論規則の話だろうか?

一階述語論理の推論規則には 「∀x.P[x] から P[t] を導く規則」や「P[t] から ∃x.P[x] を導く規則」が含まれている(ヒルベルト流でも自然演繹でもシーケント計算でも)。 ここでビミョーなのが一階述語論理では勝手に自由変数を置いて使える点。 そのため、一階述語論理では勝手に置いた自由変数tについて (∀x.P[x]) → P[t] が証明出来る。同様に P[t] → (∃x.P[x]) も証明できるため、それらから (∀x.P[x]) → (∃x.P[x]) も証明出来る。 しかし、論理式の意味を考えると、∀x.P[x] は領域が空なら真である一方で、∃x.P[x] は領域が空なら偽だし、さらに P[t] は領域が空なら解釈不能になってしまう。 これらの矛盾を避けるため、一階述語論理のモデル論では領域Dは空集合でないこと前提とされている。

一方、Coq等の基づいている型理論では自由変数を勝手に置いたり出来無いため、これらを一階述語論理の場合と同様に証明する証明することは出来ないし、またDが空集合である場合も許される。 そのため、ここでは一階述語論理を模すため、Dの要素dの存在を明示的に仮定している。

(追記: 「定数記号」と書いていた部分を「自由変数」に変更した)

λ. 『すもももももも - 地上最強のヨメ (8)』 大高 忍

読んだ。