2007-03-09 [長年日記]
λ. 女性誌がモテに使える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) を読むと、あんま都知事にはなって欲しくないなぁと思う。 私は東京都民じゃないから、都知事選には投票できないけどさ。
「Gが証明できない」仕組みと「¬Gが証明できない」仕組みが違うのでは。<br>Gって∀xF(x)の形で、「個々の具体的な整数nに関してF(n)は証明できるけど<br>∀xF(x)は証明できない」論理式だから、T∪{G}はTに公理Gを加えた拡張だけど、<br>T∪{¬G}はω矛盾しているのでは。(ω矛盾してるから、もちろん矛盾している)
ごめんなさい。以下は間違い。<br>「ω矛盾しているなら、矛盾している」<br>これは言えませんでした。<br><br>ところで酒井君、学校のアカウントって残すの?
T∪{¬G} はω矛盾ではあるけど矛盾はしていないので、モデルを作るのに問題はないはず。<br># 同様に考えると T∪{¬Con(T)} もモデルを持つのか……ちょっとビックリ。<br><br>> ところで酒井君、学校のアカウントって残すの?<br>残さないつもり。<br>半永久的に転送してくれるならともかく、一年しか転送してくれないし。<br>この日記等はそのうち移動するかもしれないけど、当面はこのままの予定。<br># そういえば、卒業生用のホストって、SFCの契約してるデータベースや電子ジャーナルは利用出来るの?
http://itc.sfc.keio.ac.jp/pukiwiki/index.php?%C2%B4%B6%C8%C0%B8%B8%FE%A4%B1%BE%F0%CA%F3<br><br>素晴しくありがたみがないと思うんだよなぁ。
女性誌読んでもモテにはつながりません。あと CanCam とかはリスク分散（？）のために彼氏は常に 2 〜 3 人はキープしておけなど平気で書かれているので、女性不信にならないためにも読まないことをお勧めします:)
考えているのは、矛盾はしてないがω矛盾している<br>モデルっすね。勘違いしてて何も解決してませんでした。<br>以下、少し調べてみました。<br>PA+¬Con(PA)は算術の超準モデルとのこと。([1]より)<br>結局、そのモデル自体はピンとこないけれど...<br>[1]「算術のモデルとその周辺」 菊池誠<br>(http://www.i.hosei.ac.jp/~ikeda/summ2005/kikuchi.pdf)<br>[2] 数学基礎論と消えたパラドックス<br>(http://members.at.infoseek.co.jp/nbz/ref/paradox.html)<br><br>> 卒業生アカウント<br>上に張っていただいたリンクをたどると、<br>商業用のデータベースなんかは使えないみたい。<br>私も更新やめようかな...<br><br>どうも長々失礼しました。それじゃ。
＞佐野さん<br>やっぱ電子ジャーナルとかは使えないのね。<br>仕方ないのだろうけど、やっぱ1万円分の価値はないねぇ。<br><br>＞alphaさん<br>がーん。僕も女性誌を読もうと思ってたのにー (笑<br><br>＞竹内さん<br>そういえば、その二つは以前何かの機会に読んだことがあります。<br>そうかー、ここで超準モデルの話と繋がるんですね……
電子ジャーナルは、酒井さんの内定先で契約しているところなら、会社経由で使えますよ。SFCのよりは圧倒的に少ないだろうけど。<br><br>図書館の利用カードとか、OBも作れるなら作っておいた方がいいかもです。（SFCの事は詳しいことはわからないけど）会社入ると、大学の図書館のありがたみがひしひしと…
昔廣瀬健先生に習った記憶では T∪{¬G}はω矛盾な理論の例です。<br>つまり、Ｇの"証明"はノン・スタンダードなものです。<br>あと、皆さんもうお分かりとは思いますが、ω矛盾してても、矛盾してるとはいえません。<br>つまり、ω矛盾は矛盾よりも強い条件です。<br>＞T∪{¬Con(T)} もモデルを持つのか……ちょっとビックリ。 <br>そうですね。驚きですが本当です。<br>つまりCon(T)は、Tの無矛盾性を完全に表現するものではない<br>ってことになります。<br>あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です。
＞たけおさん<br>おお、会社経由で使えるんですね。それは良かったです。<br>図書館の利用カードはいつでも手続き出来るようなので、とりあえず必要になったら作ればいいかなぁと思ってます(^^;<br><br>＞通りすがり さん<br>はじめまして。<br>廣瀬健先生に習ったとのことで、詳しそうで羨ましいです(^^;<br><br>> つまりCon(T)は、Tの無矛盾性を完全に表現するものではないってことになります。 <br>そうですね。<br>これは、Con(T)が真に無矛盾性を表現するためには、Tがω無矛盾でないといけないからということなのでしょうか?<br><br>> あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です。<br>なるほど。ちょっと考えて見ます。<br>情報ありがとうございました。
当然じゃないか！ サーベイ重要！