日々の流転

λ. 桜木亭パンダ焼

きもかわいい。

λ. 選択範囲のチェックボックスを一括でチェックするBookmarklet

最近、大量のチェックボックスをチェックする機会があったので、ブックマークレットを作ってみた。Firefox等のMozilla系ブラウザでしか動かないと思う。

• 選択範囲のチェックボックスを一括チェック (これをブックマーク)

コードは outsider reflex の「選択範囲のリンクを収集する 〜 DOM2 RangeのcompareBoundaryPointsの使い方」という記事のコードを少し書き換えただけで、Bookmarklet Crunchinator でブックマークレット化した。

Freakonomics読了。次は何を読もう。Harry Potter にでもするかなぁ。

λ. I/Oとアイドル

ふと「アイドルはウンコしない」と「純粋関数型言語には副作用はない」は似ているのではないかと思った。 考えてみれば食事や排泄はI/Oである。 ふと思っただけで、深い意味はないが。

λ. 健康診断

内定先の健康診断に行ってきた。

λ. ⊤⊤-closed relations and admissibility by Martín Abadi

一ヶ月前にKeisukeNakanoさんに紹介してもらったのをようやく読んだ。

メモ

Theorem 2 の証明の前半では R⊇{(a,b)∈A×B | a b ∧ b a} だけ示して R⊆{(a,b)∈A×B | a b ∧ b a} は示していないが、後者は R ⊆ と R^-1⊆ より自明。

Theorem 2 の証明の後半では R が TT-closed であることを示すのに、¬(a R b) ⇒ ¬(a R^TT b) を示しているが、a R^TT b ⇒ a R b を示すようにした方が全体の流れが分かりやすくなると思った。

Corollary 3 の「It follows that: a R b ≡ a b ∧ b a」の部分は以下から言える。

• ⊆ より、a b ∧ b a ⇒ a b ∧ b a ⇔ a R b
• R ⊆ と R^-1 ⊆ より、a R b ⇒ a b ∧ b a

λ. 今日の英語: Don't count on anyone except yourself.

「誰にも頼るな」という意味。

λ. 女性誌がモテに使える5つの理由

研究室の某氏の机の上には時々女性誌が置いてあるのだが、あれにはこんなメリットがあったのだな、と思った。

λ. 不完全性定理に関して混乱中

Tを(第一)不完全性定理が適用可能なセオリー、GをTでのゲーデル文とする。 すなわち、T ⊢ G≡¬(∃x. prove(x,[G])) で、また T ⊢ prove(p,a) は「aはある論理式Aのゲーデルコーディングであり、pは T⊢A のある証明図πのゲーデルコーディングである」ことと同値であるとする。

Tがω無矛盾ならば、Tでは G も ¬G も証明できない。 ということは、Tがω無矛盾なら T∪{G} も T∪{¬G} も無矛盾なわけで、それぞれモデルが存在する。 前者のモデルでは「G は真だけど証明できない」ということになり、Gの「自分は証明できない」という直観的な意味にマッチしていて、なんとなく理解出来る気がする。

しかし、後者のモデルは直観的にはどう理解すればよいのだろうか?　 このモデルでは ¬G が真であり、したがって ∃x. prove(x,[G]) も真である。 この x はモデルの外から見れば当然 T ⊢ G の証明図を表してはいないが、モデルの中からみれば T ⊢ G の証明図を表しているのだろうか?　もしそうだとすると、このモデルの中からはTがω矛盾しているように見えるのか?

多分、非常に基本的かつ簡単なことだと思うのだが、混乱中。 情けない……

λ. SFCから都政へ挑戦!　浅野史郎教授が都知事選に出馬表明

浅野史郎氏ってSFCの教授だったのか。知らなかった。 しかし、 小熊さんの意見 や 泥酔論説委員の日経の読み方(2007-03-04) を読むと、あんま都知事にはなって欲しくないなぁと思う。 私は東京都民じゃないから、都知事選には投票できないけどさ。

λ. 不完全性定理に関して混乱中 (2)

不完全性定理に関して混乱中の続き。 かがみさんの「モデルでの真偽」というエントリを読んで、考えてみる。

第二不完全性定理の証明では第一不完全性定理の算術化が必要なので、第一不完全性定理で使う概念は、ω無矛盾性を含めて全て算術化可能なのではないかと思います*1。 Tのω無矛盾性は「任意のnについて T ⊢ P(n) ならば T ⊬ ∃x. ¬P(x)」だから、 provable(x) := ∃y. prove(y,x) と定義すると、 ωCon(T) := ∀[P]. (∀n. provable([P(n)])) → ¬provable([∃x. ¬P(x)]) のような感じで算術化可能なはず(表記は少し誤魔化してるけど)。

そうすると、私の知りたかったことは、大体「M ⊧ T∪{¬G} のとき M ⊧ ¬ωCon(T) や M ⊧ provable([¬ωCon(T)]) は成り立つのか?」になるのかな……

まず、M ⊧ ¬ωCon(T) について考えてみる。 T ⊢ Con(T)→¬provable([G]) と T ⊢ G≡¬provable([G]) から T ⊢ Con(T)→G 。 対偶をとって T ⊢ ¬G→¬Con(T) で、したがって T∪{¬G} ⊢ ¬Con(T) 。 完全性定理から T∪{¬G} の任意のモデルMで M ⊧ ¬Con(T) 。 M ⊧ ¬ωCon(T) だけでなく M ⊧ ¬Con(T) まで成り立つのだな(考えてみればあたりまえだけど)。

次に、M ⊧ provable([¬Con(T)]) について考えてみる。 T∪{¬G} ⊢ ¬Con(T) ということは任意の論理式Aについて T∪{¬G} ⊢ provable([A]) であり、従って T∪{¬G} ⊢ provable([¬Con(T)]) 。ということは、M ⊧ provable([¬Con(T)]) も言える。

結論。Mの中で形式化したTは矛盾している。 そして、矛盾してしまったのは、超自然数に対応する証明図がある分、証明能力が強くなっているため。 疑問は解けたが、なんだか少し不思議な感じがするなぁ。

λ. 世界一の債権国、日本に味方はいない

<URL:http://www.h-yamaguchi.net/2007/03/post_3683.html> より。 後で読む。

λ. 算術的階層の厳密性と形式的手法の限界について

を読んでいる途中。 算術的階層って難しいものだとばかり思っていたけど、定義は簡単だし、しかもこんなに役に立つものだったんだな。

λ. 不完全性定理に関して混乱中 (3)

前回のエントリで元々の疑問は大体解決しました。 色々とコメントや言及をありがとうございます。

特に、竹内さんと通りすがりさんのコメント、かがみさんのエントリ(モデルでの真偽, さらにω矛盾)は疑問を解消する上で大いに役立ちました。

また、あろはさんにも二つのエントリで言及していただきました。

• 真なのに証明できない命題 ？？？
• 「不完全性定理に関して混乱中」に関して混乱中

以下、色々と余談みたいなものを。

何故こんな疑問を持ったか?

そもそも、何故こんな疑問を持ったかというと、きっかけはTaejun(태준)さんという方のブログTaejunomicsの「数学と法律はかなり近い？」というエントリに以下のように書いてあったこと。

述語論理の公理系に、等号の公理と数の公理が加わっただけで、その体系は数学の公理系になります。　ちなみに、この二つを加えることによって、完全な述語論理の体系が、不完全になってしまうらしく、これをゲーデルの不完全性定理というそうですね。　（完全とは、その公理系が妥当な論理法則の全てを証明することが出来る事を指します）

これに「完全性定理と不完全性定理の『完全性』は違う意味*1で、等号の公理と数の公理を加えることによって『完全性』が損なわれるわけではない」というような内容のコメントを書こうとして、「そういや、算術の体系に完全性定理を適用するとどうなるんだっけ?」と思い、9日の混乱(不完全性定理に関して混乱中)に至ったのでした。

不完全性定理に言及することについて

あろはさんの二つのエントリは幾つか勘違いしている気がするけど、それはとりあえず横に置いておいて、ちょっと別の話を。

あろはさんは真なのに証明できない命題 ？？？というエントリで「数学をちゃんとやってない俺が書いて良いような内容じゃないし… おこがましすぎる」と書いている。 けど、不完全性定理自体は基礎的な定理だし、前提知識も少ないので、ちょっと論理学を勉強すればすぐに理解できるはず。 「おこがましすぎる」等と言う前に、ちょっと勉強すれば良いだけだと思います。

実際、今回使ったのは向井先生の「数学と論理」*2という授業で得た知識くらいで、この授業は主に学部1年生が履修する授業です。

「通りすがり」さんの問題

「通りすがり」さんのコメントの「あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です」について考えてみる。

T ⊢ provable([G])→G と仮定する。 T ⊢ G≡¬provable([G]) より T ⊢ ¬provable([G])→G 。 T ⊢ provable([G])∨¬provable([G]) なので T ⊢ G 。 これは第一不完全性定理に矛盾するので、背理法より T ⊬ provable([G])→G 。 というわけで、T ⊢ provable([P])→P は一般には言えない。

次に、あるPについて provable([P])→P の否定が真であるモデルMを考える。 すなわち M ⊧ T∪{¬(provable([P])→P)} で、¬(provable([P]→P) ≡ provable([P])∧¬P だから、 当然 M ⊧ provable([P]) かつ M ⊭ P になる。 モデルが非健全という言い方には少し違和感を感じるけど、言わんとすることは理解できる。

残る疑問点

今回のことで不完全性定理についてだいぶ理解を深められた気がするが、まだ残っている疑問も幾つかある。

その一つはロッサーの不完全性定理が何故成り立つのかという事。 ゲーデルの証明ではω無矛盾性を条件としていたが、後にロッサーがω無矛盾性を無矛盾性に弱めている。 今回、ω無矛盾性を条件としたのは、これが何故成り立つのか知らなかったから。 聞くところによると、ゲーデル文とは違う文を考えるらしいが……

あとは、論理学にまつわるトンデモ言説「自分自身の無矛盾性を主張する文は証明できない」の以下の記述について。

標記の主張は、自分自身の無矛盾性を主張するすべての文は、証明できない、ということになってしまします。これは少くとも、通常ゲーデルの不完全性定理の対象とされるペアノ算術では正しくありません。実際に、自分自身(つまりペアノ算術)の無矛盾性を主張している(と理解できる)が、しかしペアの算術で証明できてしまう文が存在するのです。

これらはまたの機会にでも考える。

【追記】 と書いたら、かがみさんの「ロッサーの不完全性定理」でどっちも解決してしまった。もきゅ(´・ω・`)

λ. ω矛盾かあちゃん

ω無矛盾 - Wikipedia に載っている「ω矛盾かあちゃん」に笑った。元ネタの詩が知りたい……

論理学者のレイモンド・スマリヤンは、ルイス・キャロルの詩をオマージュしてω矛盾を諧謔的に説明した。(ω矛盾かあちゃん)。

母親「あれはしちゃだめ、これもしちゃだめ…」 子供「ねぇ、何かしていい事はあるの？」 母親「ええ、あるわよ。でもあれもだめ、これもだめ…」

λ. 「相棒」最終回

今回は幾らなんでも設定に無理がありすぎじゃないかと。 まあ、私の好きな小野田官房長が沢山登場したので許すけど(おい)。

GPS(Global Positioning System)が座標だけでなく地図情報まで提供してたとは驚きだし、それにGPSの脆弱性を利用してGPSに影響を与えるプログラムが仮にあったとして、それが軍事的な優位に繋がることはないだろう。存在が明らかになれば対策されるに決まっているから、一回使ったらそれで終わりで、存在を抑止力にすることは出来ない。 そもそも、日米同盟があれば、安全保障上の必要から民生用の信号の精度を低下させる事はある程度可能だろうし、脆弱性を利用するメリットはない。そして、日米同盟が解消された場合や、相手が軍事目的の信号を利用できる場合であれば、それはもはやGPS云々の問題では済まないだろうに。

あと、地方公務員法の第49条の2「前条第1項に規定する処分を受けた職員は、人事委員会又は公平委員会に対してのみ行政不服審査法による不服申立て(審査請求又は異議申立て)をすることができる」と第50条「第49条の2第1項に規定する不服申立てを受理したときは、人事委員会又は公平委員会は、直ちにその事実を審査しなければならない。この場合において、処分を受けた職員から請求があつたときは、口頭審理を行わなければならない。口頭審理は、その職員から請求があつたときは、公開して行わなければならない」を利用していたのが面白かった。

λ. ロッサーの不完全性定理

かがみさんの「ロッサーの不完全性定理」と通りすがりさんのコメントで情報としては十分過ぎるけど、ちょっと考えたこともあるので一応メモ。

ロッサー文

prove´(x,[A]) := prove(x,[A]) ∧ (∀y≦x. ¬prove(y,[¬A])) として、 T ⊢ R≡¬∃x. prove´(x,[R]) を満たす論理式Rをロッサー文という。 T ⊢ R≡(∀x. prove(x,[R]) → ∃y≦x. prove(y,[¬R])) なので、通りすがりさんが書いているように、Rの直観的な意味は「この命題の証明が存在すれば、この命題の否定のより簡単な証明が存在する」となる。

補題1: T ⊢ A ならば ∃x. prove´(x,[A])

T ⊢ A と仮定する。

1. その証明図πが存在し T ⊢ prove([π],[A])。
2. Tの無矛盾性より T ⊬ ¬A であり、任意の x≦[π] について T ⊢ ¬prove(x,[¬A]) 。したがって、 T ⊢ ¬prove(0,[¬A])∧¬prove(1,[¬A])∧…∧¬prove([π],[¬A]) であり T ⊢ ∀x≦[π]. ¬prove(x,[¬A]) 。

したがって、T ⊢ ∃x. prove´(x, [A])

T ⊬ R

T ⊢ R と仮定する。

1. 補題1より T ⊢ ∃x. prove´(x, [R])
2. 一方、T ⊢ R≡¬∃x. prove´(x,[R]) より T ⊢ ¬∃x. prove´(x,[R]) 。

これは矛盾なので、背理法より T ⊬ R 。

補題2: ある定数nについて T ⊢ ∃x≦n. prove(x, [A]) ならば T ⊢ A

T ⊬ A と仮定し、nを任意の定数とする。 任意のx≦nについて T ⊢ ¬prove(x,[A]) であるので T ⊢ ¬prove(0,[A])∧¬prove(1,[A])∧…∧¬prove(n,[A]) で T ⊢ ∀x≦n. ¬prove(x,[A]) 。 すなわち T ⊢ ¬∃x≦n. prove(x,[A]) で、Tの無矛盾性より T ⊬ ∃x≦n. prove(x,[A]) 。

T ⊬ ¬R

T ⊢ ¬R だと仮定する。

1. その証明図πが存在して T ⊢ prove([π], [¬R])
2. 一方、T ⊢ R≡¬∃y. prove´(y,[R]) より T ⊢ ∃y. prove(y,[R]) ∧ ∀z≦y. ¬prove(z,[¬R])

ここから T ⊢ ∃y. prove(y,[R]) ∧ ¬([π]≦y) で、簡単な定理を適用すると T ⊢ ∃y<[π]. prove(y,[R]) が得られ、補題2より T ⊢ R 。 これはTの無矛盾性に矛盾するので、背理法より T ⊬ R 。

考察

巧妙なのは、「T ⊢ ∃x. prove(x,[A]) ならば T ⊢ A」にはω無矛盾性が必要なのに対して、補題2の「ある n について T ⊢ ∃x≦n. prove(x,[A]) ならば T ⊢ A」には無矛盾性で十分なこと。そして、それが利用できるように論理式Rを構成した点か。ゲーデルのアイディアに比較すれば技術的な微調整に過ぎないかもしれないけど、こういうのも好きだし感心。

算術的階層との関連で考えると、 ∃x. prove(x,y) は Σ₁ であって Δ₁ ではないのに対して、 ∃x≦n. prove(x,y) は Δ₁ というのが効いているのだろうと思う。

次は「クライゼルの注意」について考えるか。

λ. 堀江被告に実刑2年6月「一般投資家欺いた」

有罪自体はそこまで意外ではないけど、実刑になったのは意外。 証取法で実刑なんて結構珍しいのでは。

それと、「堀江被告、即金2億円で再保釈　保証金は5億円」を見て思ったのだが、保釈金って法定利息が付いたりするのだろうか?　……どうやら付かないらしい。供託金には利息がつく*1のに保釈金には付かないというのは少し気持ち悪い気がする。

λ. クライゼルの注意

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

φ := ∃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を喰らっているようなので、このページにもアクセスしにくいかも。 私はサーバ管理にはあまり詳しくないので、対処はまかせっきりなのだけど、中々大変そうだ。

λ. 『マオ—誰も知らなかった毛沢東 (下)』

を読んだ。 どこまで信じてよいのかは分からんが、とにかく面白い。

上巻は共産主義体制を確立し最高指導者の地位に上りつめるまでの話だったが、下巻はそこから死ぬまでの話。毛沢東は上巻にに続いて権謀術数に心血を注ぎ、自らの権力と目的のためならば何千万の国民を餓えさせることも厭わない。 絶対に関わりあいたくない人物だけど、その一方で、道徳に縛られず純粋に自らの権力のためにこれだけの事をやってのける毛沢東像は非常に魅力的な悪役であるとも思った。 さすが毛沢東!　俺達にできないことを平然とやってのけるっ!　そこに痺れる!　憧れるうぅ!　って感じで。

λ. 『論理の哲学』 飯田 隆

を読んだ。

λ. 『日本の外交は国民に何を隠しているのか』 河辺一郎

を読んだ。

λ. エネミーライン

を観た。

λ. バンディッツ

を観た。

λ. ゴッドファーザー PART III

を観た。

λ. 「Haskell の call/cc 重大な設計ミスか！？」

PPL2007の「合成モナドのためのcall/ccに対する改善の提案」(米澤拓央 (筑波大学))って、どういう話だったのだろうか。ちょっと気になる。

λ. ショコラ

ショコラ【廉価2500円版】 [DVD]を観た。 ほのぼの。お腹が空いていたのでチョコを食べたくなった。

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

今日は圏論勉強会というか『量子ファイナンス工学入門』勉強会だった。 写真。

λ. 萩野・服部研 2006年度納会

＠海老専家

λ. 証明書発行

就職先に提出する修了証明書と成績証明書を発行してもらいに学校へ。23日までに申し込んでいれば学位授与式で学位記と一緒にもらえたのだが、申し込むのを忘れてたので。あと、明日までは即日発行可能なのに、30日に申し込むと4/2以降の発行になってしまうというのが不思議。

λ. Edyが使えるコピー機

生協のコピー機を使おうとしたら、Edyが使えるやつがあってビックリした。

λ. 学位授与式

というわけで、学士(総合政策)から修士(政策・メディア)に。