日々の流転

λ. クライゼルの注意

かがみさんの「ロッサーの不完全性定理」で紹介されていた、「クライゼルの注意」を示してみる。

φ := ∃x. prove´(x, [0=1]) とする。

1. T ⊢ φ → (∃x. prove(x,[0=1]) ∧ (∀y≦x. ¬prove(y,[¬(0=1)]))) であるので、T ⊢ ¬(0=1) のある証明図をπとすると、T ⊢ φ → (∃x≦[π]. prove(x,[0=1])) 。
2. 一方、Tの無矛盾性より T ⊬ 0=1 なので、T ⊢ ¬∃x≦[π]. prove(x,[0=1]) 。

よって、T ⊢ ¬φ 。

最初は何故成り立つのか不思議だったけど、20070316#p01でロッサーの不完全性定理を理解したら、あとは自明だった。

λ. DDoSうざい

ここ数日、散発的にDDoSを喰らっているようなので、このページにもアクセスしにくいかも。 私はサーバ管理にはあまり詳しくないので、対処はまかせっきりなのだけど、中々大変そうだ。