トップ «前の日記(2007-03-07) 最新 次の日記(2007-03-11)» 月表示 編集

日々の流転


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がω矛盾しているように見えるのか?

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

Tags: logic

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

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

Tags: 時事
本日のツッコミ(全11件) [ツッコミを入れる]
ψ 竹内 (2007-03-10 13:21)

「Gが証明できない」仕組みと「¬Gが証明できない」仕組みが違うのでは。<br>Gって∀xF(x)の形で、「個々の具体的な整数nに関してF(n)は証明できるけど<br>∀xF(x)は証明できない」論理式だから、T∪{G}はTに公理Gを加えた拡張だけど、<br>T∪{¬G}はω矛盾しているのでは。(ω矛盾してるから、もちろん矛盾している)

ψ 竹内 (2007-03-10 13:42)

ごめんなさい。以下は間違い。<br>「ω矛盾しているなら、矛盾している」<br>これは言えませんでした。<br><br>ところで酒井君、学校のアカウントって残すの?

ψ さかい (2007-03-10 22:23)

T∪{¬G} はω矛盾ではあるけど矛盾はしていないので、モデルを作るのに問題はないはず。<br># 同様に考えると T∪{¬Con(T)} もモデルを持つのか……ちょっとビックリ。<br><br>> ところで酒井君、学校のアカウントって残すの?<br>残さないつもり。<br>半永久的に転送してくれるならともかく、一年しか転送してくれないし。<br>この日記等はそのうち移動するかもしれないけど、当面はこのままの予定。<br># そういえば、卒業生用のホストって、SFCの契約してるデータベースや電子ジャーナルは利用出来るの?

ψ 佐野 (2007-03-10 22:35)

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>素晴しくありがたみがないと思うんだよなぁ。

ψ alpha (2007-03-11 00:15)

女性誌読んでもモテにはつながりません。あと CanCam とかはリスク分散(?)のために彼氏は常に 2 〜 3 人はキープしておけなど平気で書かれているので、女性不信にならないためにも読まないことをお勧めします:)

ψ 竹内 (2007-03-11 00:52)

考えているのは、矛盾はしてないがω矛盾している<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>どうも長々失礼しました。それじゃ。

ψ さかい (2007-03-11 03:00)

>佐野さん<br>やっぱ電子ジャーナルとかは使えないのね。<br>仕方ないのだろうけど、やっぱ1万円分の価値はないねぇ。<br><br>>alphaさん<br>がーん。僕も女性誌を読もうと思ってたのにー (笑<br><br>>竹内さん<br>そういえば、その二つは以前何かの機会に読んだことがあります。<br>そうかー、ここで超準モデルの話と繋がるんですね……

ψ たけを (2007-03-11 12:43)

電子ジャーナルは、酒井さんの内定先で契約しているところなら、会社経由で使えますよ。SFCのよりは圧倒的に少ないだろうけど。<br><br>図書館の利用カードとか、OBも作れるなら作っておいた方がいいかもです。(SFCの事は詳しいことはわからないけど)会社入ると、大学の図書館のありがたみがひしひしと…

ψ 通りすがり (2007-03-12 09:12)

昔廣瀬健先生に習った記憶では T∪{¬G}はω矛盾な理論の例です。<br>つまり、Gの"証明"はノン・スタンダードなものです。<br>あと、皆さんもうお分かりとは思いますが、ω矛盾してても、矛盾してるとはいえません。<br>つまり、ω矛盾は矛盾よりも強い条件です。<br>>T∪{¬Con(T)} もモデルを持つのか……ちょっとビックリ。 <br>そうですね。驚きですが本当です。<br>つまりCon(T)は、Tの無矛盾性を完全に表現するものではない<br>ってことになります。<br>あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です。

ψ さかい (2007-03-13 02:34)

>たけおさん<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>情報ありがとうございました。

ψ 某氏 (2007-03-22 16:52)

当然じゃないか! サーベイ重要!