日々の流転

λ. ¬(∀x.P(x)) → ∃x.¬P(x)

非常にしょーもないのだが、ふと ¬(∀x.P(x)) → ∃x.¬P(x) の証明を自然演繹で書こうとして苦戦。こんな基本的な事で苦戦するなんて色々やばいな。 結局、callccを使ったプログラムを思い浮かべて証明した。 古典論理はやっぱり変態的だと思った。

Agdaでの証明

postulate callCC (|X::Set) :: Not (Not X) -> X

prop (!D::Set) (!P::D->Set)
    :: Not ((x::D) -> P x) -> Exist (\(x::D)-> Not (P x))
prop k1 =
    callCC (\(k2::Not (Exist (\(x::D) -> Not (P x)))) ->
        let f :: (x::D) -> P x
            f x = callCC (\(k3::Not (P x)) ->
                      let e :: Exist (\(x::D) -> Not (P x))
                          e = struct
                                fst :: D
                                fst = x
                                snd :: Not (P x)
                                snd = k3
                      in k2 e)
        in k1 f)

自然演繹での証明

Agdaによる証明をそのまま翻訳したもの。

[¬P(x)]:3
───── (∃I)
∃x.¬P(x)    [¬∃x.¬P(x)]:2
─────────────── (¬E)
⊥
───── (¬I{3})
¬¬P(x)
───── (¬¬)
P(x)
───── (∀I)
∀x. P(x)       [¬∀x.P(x)]:1
─────────────── (¬E)
⊥
─────── (¬I{2})
¬¬∃x.¬P(x)
─────── (¬¬)
∃x.¬P(x)
─────────────── (→I{1})
¬∀x.P(x) → ∃x.¬P(x)

シーケント計算での証明

自然演繹だとややこしかったけど、シーケント計算だと実は簡単。

P(a) ├ P(a)
──────── (├ ¬)
├ P(a), ¬P(a)
──────── (├ ∃)
├ P(a), ∃x.¬P(x)
────────── (├ ∀)
├ ∀x.P(x), ∃x.¬P(x)
──────────── (¬ ├)
¬∀x.P(x) ├ ∃x.¬P(x)
─────────────── (├ →)
├ ¬∀x.P(x) → ∃x.¬P(x)

λ. 第三十二回圏論勉強会

今日は圏論勉強会だった。

λ. 『ηなのに夢のよう』 森博嗣

Gシリーズはやっぱり西之園萌絵の成長がテーマだったのだなと思った。 綺麗な終わり方。 肝心のところは引っ張っるだけ引っ張ってそのままだけど。