08/20 かがみ  08/20 miya  07/24 Tsubaki  07/24 かが☆みん  07/24 Tsubaki  07/24 良い子のかが☆みん   

2009年10月31日(金)

• 数学基礎論講演会〜ゲーデルの不完全性定理

  今日は東工大で田中先生の「数学基礎論講演会〜ゲーデルの不完全性定理」で した。 １回目の講演会 に続き今回は2回目です。

  面白かったです。楽しかったです。

  ヒルベルトの計画から始まり、ゲーデルの不完全性定理の概説、そしてその後 の発展を分かりやすく説明して頂きました。実はアイディアの部分に関しては それを鵜呑みにすると容易にトンデモとなりうる要素もありえたと思うのです が、田中先生はその点についても十分配慮され、さらに「非専門家向け」とい う割には、聴衆者はそれなりの予備知識を持った人ばかりという感じだったの でその心配は全くなさそうです。もちろん不完全性定理が成立する条件につい ても非常に詳しく説明して頂きました。

  一番驚いたのは次の定理です。

  PA |- (Bew([A]) -> A) のとき PA |- A

  証明可能であることが証明可能であることを仮定して証明できれば証明できる なんてびっくり仰天です。知りませんでした。上の主張をヘンキン文と言い、 Löb により正しいことが証明されたそうです。

  今まで不勉強だったのですが PA を含む無矛盾な体系で Π_1 文が証明されれ ばそれが「真である」と確信を持てるが例えば ZFC で Σ_1 文を証明した場合 ZFC の Σ_1 健全性を仮定しない限り「真」とは言えない可能性があるお話も 面白かったです。

  最後の質問で、「そもそも真とはなんでしょうか」などと余計な質問をしたこ とについてはご容赦の程お願いいたします。でもちらっと標準モデルで成り立 つことという事実を教えて頂いたのは本日の大きな収穫です。なんとなくそん な気がしていたのですが確信がなかったのです。

  tri_iro さん と igarisさん にお会いすることができました。tri_iro さんと は2年前に静岡で一度お会いしました。そのときこれでもうお会いすることは ないかなと思ったのですが、もう一度お話が出来たのはとてもうれしかったで す。写真一緒に撮ってくださいとかお願いを色々してご迷惑おかけしました。 尊敬する人と一緒の写真に写ってみたいんです。

  igaris さんとはネットでは色々お話する機会があったのですが、今日始めて お会いしました。色々楽しいお話をすることができてとても有意義な時間を 過ごしました。ありがとうございます。

  講演会の後 mushitoriseinenさん と顔合わせしたかったのですが、主に私の配慮不足で会い損ねてしまいま した。非常に残念です。申しわけなかったです。

  この催しは今後も少なくとも後一回は行われる予定だそうです。たのしみにし ています。

  コメント

  _igaris [こちらこそ、とても楽しい時間を過ごさせて頂きました。ありがとうございました。Σ_...]

  _mushitoriseinen [本日はおつかれさまでした。いやぁ、楽しかったですね。ぼくは第一不完全性定理の別証...]

  _かがみ [今日は本当に楽しい時間を過ごさせて頂きありがとうございます。ゴールドバッハについ...]

  _かがみ [いや。本当に申しわけございませんでした。みなみさんは髪の毛たくさんあったじゃあな...]

  _tri_iro [こちらこそ、かがみさんと久しぶりにお話が出来て楽しかったです。東工大での写真、先...]

  _かがみ [写真頂きました。ありがとうございます。色々お世話になりました。出来ればまたお会い...]

  _てなさく [＞ PA |- (Bew([A]) -> A) のとき PA |- A こ...]

  _てなさく [証明できたと書きましたがよく見たら間違ってました... ションボリ...]

  _標準モデル [健全性の話は不完全性関係の専門書じゃないと載ってませんが、Loebの定理は最近の...]

  _かがみ [てなさくさんがご存知なかったとはちょっと意外でした。「ゲーデルと20世紀の論理学...]

  _ふちの [ええと，これではだめなんでしょうか:PA|- Bew(A) -> A なら...]

  _かがみ [あ。たしかにそのような気がします。すると一つ前の私のコメントは誤読でした。失礼い...]

  _ふちの [ついでに言うと，「標準モデルで成り立つこと」というのはいかにも田中さんらしいです...]

  _ふちの [今回このコメント欄では誰も問題にしていませんでしたが，PA |- (Bew([A...]

  _かがみ [実はその言葉 (もしかして「真」とは「標準モデルで成り立つ」ということですか？)...]

  _てなさく [かがみさん＞てなさくさんがご存知なかったとはちょっと意外でした。Enderton...]

  _てなさく [うわっまたやってしまった。「誤読でした」はかがみさんの発言でした。てなさくが誤読...]

  _てなさく [ああっとつまり何が言いたいかというと、¬Bew[A] は PA+¬A のcons...]

  _てなさく [いずれにせよ粗忽なコメントを乱発してかがみさんとふちのさんにご迷惑をおかけしまし...]

  _かがみ [色々教えて頂き感謝しております。ですが頭が混乱してきたのでしばらくこの話題にかん...]

  _通りすがり [ふちの氏のいわれる証明は、ブーロス＆ジェフリーの本"Computabi...]

  _通りすがり [＞「(Bew([A]) -> A) の PA からの証明が与えたれたときに...]

  _かがみ [通りすがりさん、コメントありがとうございます。何か一言書きたいところですが完全に...]

  _通りすがり [↓でいいように思うのだが。PA |- (¬CONS -> Bew(A))な...]

  _通りすがり [↑は最後の"不完全性定理より…"が誤りだった。全然ダメじゃん...]

  _かがみ [通りすがりさん、こんにちは。もう本当についてゆけません。気の利いたコメント書けな...]

  _通りすがり [第二不完全性定理に関しては、あくまでBewの定式化次第だ、ともいわれてます。Ro...]

  _かがみ [すみません。こちらの方は頭が飽和してついてけない状態です。Bew の解釈はなんと...]

• つくば出張

  今日から金曜日までつくばに出張です。

  コメント

• 数学ガール/ゲーデルの不完全性定理

  会社宛に届くように注文したのが届きました。実はおうちのほうには頂きもの の方が先週の金曜日に届いてたのですが、なんか汚したりするのがもったいな くてまだ読んでいません。ごめんなさい。これで真面目に読むことができます。 とはいえ仕事中には読めないのと今週も府中に缶詰めという感じなので、真面 目に読むのは週末になるかも知れません。もちろん社長のところにじまんしに 行きました。私はなにもしていませんが自慢だけはちゃんとするのです。

  ゲーデルの不完全性定理について30秒で説明しましたが分からないみたいです。 当然です。でも社内報に載せてくれるとか何とか。やはりじまんしに行ったの は正解のようです。

  というわけで少々時間かかるかも知れませんが、この日記で感想を書く予定で す。思い出すと本当に楽しいレヴューでした。あんな楽しい体験は一生のうち 何度もあるとは思えません。素晴らしい体験をさせて頂いた結城さんに感謝い たします。

  (追記) 会社で3冊営業。

  コメント

  _結城浩 [営業ありがとうございますm(_ _)m 鏡さんにはもう半端無くお世話になりました...]

  _かがみ [自分は俗物でさらに自己顕示欲が非常に強いので本に名前が載るのはとてもうれしいです...]

• ちょっと寄り道

  昨日 Devlin 本を読む予定と書きましたが選択公理をやや弱めた仮定に関する色々 面白い実例が [1] に記載されていることを知りました。いちばん驚いたのが次 の定理です。

  自然数 に対して を ZF 上の次の言明とします。

  個の要素の集合からなる任意の集合族に対する選択関数が存在する.

  は靴下洗濯公理と呼ばれています (嘘)

  びっくり仰天だったのは ZF 上で は証明可能 (これは簡単) なのに が証明不可能 (これは色々予備知識が必要そう) であるという事実です。一般に 次の事実が成立するそうです。

  を自然数として次の条件が成立すると仮定する。

  
  (1) を より (真に) 大きい素数の有限列とするとき となる分解は存在しない。
  (2) 任意の に対して がなりたつ。

  このとき も成り立つ。

  はその系となるわけです。 さらに任意の に対して が成立しても「有限集合からなる集合族への選択関数が存在する」とは言えな いそうです。興味を持ったときが勉強するチャンスです。さらになんとなくマ ニアックで余り役に立ちそうもないところも好みです。なのでちょっとの間こ ちらに浮気する予定です。

  [1] Thomas J. Jech, The Axiom of Choice, North-Holland, 1973. Reissued by Dover Publications, 2008.

  コメント

  _てなさく [うちでは靴下を洗濯するたびに一足のペアの片方が紛失します。靴下紛失公理のモデルで...]

  _かがみ [靴下紛失公理のモデルは少なくとも二つ存在することが証明されたようです。http:...]

  _ふちの [これは Tom Jech の本には載っていないかもしれませんが、実は C_2 と...]

  _かがみ [実は n<m のとき C_m → C_n が成り立つとは限らないのかそれと...]

  _てなさく [C_2→C_4 わかりました。ひとヒネリあって面白かったです。]

  _てなさく [わたくしが考えた C_2→C_4の証明を見て思うに、集合族の濃度にたとえば「可算...]

  _かがみ [私の勘違いでなければ The Axiom of Choice の C_2 → C...]

  _てなさく [かがみさんにメールしようとしたのですが未明にありがちなことでSMTPサーバが寝て...]

  _ふちの [もう気付かれているかもしれませんが、n<m のとき C_m → C_n が...]

  _かがみ [てなさくさん。ふちのさん。コメントありがとうございます。選択公理使えないんだ.....]

  _てなさく [昨晩述べた疑問 [てなさく 2009-10-28 21:18:26] に関連して...]

  _かがみ [恐ろしく返信が遅れて申しわけございません。双方読ませて頂きました。ありがとうござ...]

• 仕事を忘れる

  この3ヶ月くらい土日も含めて二つ並列の仕事のことが頭から離れませんでした。 結果的に同じことを行う必要があるのですが、一つの仕事に専念できる環境を 作ってもらいました。今週の月曜日からです。仕事がはかどることはかどるこ と。精神的にゆとりがある状態はとても大切だと実感しました。明日と明後日 は久しぶりに仕事のことを完全に忘れる予定です。Devlin 本の四章を読み始め ます。

  コメント

• 流れ星

  今の時期はオリオン座流星群がよく見えるそうなので、零時過ぎからベランダ で何度か星空をみていました。最初オリオン座の辺りをぼんやり眺めていたの ですが全然見えません。一度退散しネットで調べたところオリオン座というよ りベテルギウスと双子座の中間点近傍を眺めるのがよいそうな。余談ですがこ の歳まで「べ」テルギウスのことを「ぺ」テルギウスだと思っていました。

  再度挑戦しましたがちっとも見えません。

  うーん。大気の状態がいまいちなのかなあ。もちろんメガネはいつも使ってい る遠方の視力が 0.3 となる老眼鏡 (普通の人には非常にきつい近眼用) ではな く、視力が 1.2 となるテレビや映画用のものを使いました。それでも見えませ ん。久しぶりに 1.2 の視力で回りを見るとくっきりして良いものです。でもこ のメガネで本や PC を見ると全く文字が読めません。遠近両用でなにか呪文を 唱えると若い人の水晶体のように屈折率が変化するものがあれば良いのに。

  そんなこんなで特に何かするということもなく起きていたら、奥さまも「何し ているの？」と起きてきました。流れ星観察をしていることを話したところ奥 さまも参戦です。なんと奥さまは５分間くらいで3回も見えたそうな。なのに私 は１回も見えません。目の善し悪しというよりパターン認識や集中力に差があ るようです。

  流れ星観察は失敗しましたが、星空を眺めるのは良いものです。もちろん今日 は双眼鏡のように視野を狭くする道具は使いませんでしたが、真冬で大気の状 態が良好な場合、オリオン座周辺を双眼鏡で見ると本当に綺麗です。少し天頂 のほうに双眼鏡を向ければプレアデス星団もはっきり見えます。藤沢のように 星空を見るのに余り適した場所でなくてもある程度条件が良い場合十分楽しめ ます。とはいえたまには田舎のほうで落ちてくるような満天の星空を見たいな とも思います。出不精なのが最大のネックです。

  コメント

• みぎひだり

  私は左右の認識がまったくだめです。まず自分の右手が分からない。いや、分 かるんですけど、どっちが右手かなと考えるとき、私は右利きなので自分が鉛 筆もしくはお箸を持っている図を想像する過程を経る必要があります。向かい 合っている人の右手がどっちかはさらに大変です。まずお箸方式で自分の右手 を確認して相手さまの右手はその反対側とか。相手様の左手ともなると、自分 の右手の確認、その反対側としての自分の左手の確認、その反対側としての相 手様の左手の確認、と3段階もの推論を行う必要があります。

  相撲を観ているときの左四つと右四つは絶望的です。相撲なんでも辞典による と左四つとは組み合った状態で左手が相手の右手の内側に入っていて、さらに もろ差しになっている、もしくはなられていない状態と定義されています。昔 ならばがっぷり四つの相撲も多く認識可能な場合も多かったのです。ただし片 方の力士がテレビの画面方向にお尻を向けている場合はその力士を基準として どちらの四つか分かるのですが、双方横向きの場合途方に暮れるしかありませ ん。最近の相撲はスピードが重視されるのでさらに困ります。

  朝青龍のお尻が見える。
  自分がお箸をもつ図を想像する。
  朝青龍の右手が分かる。
  その右手が内側か外側かを認識する。
  反対側の手を見て片方の力士がもろ差し状態でないかを確認する。

  なんと５段階もの推論を行う必要があります。ところがスピード相撲の影響に より、やっとの思いで５段階のうちの3段階位目を認識した時点で向きが変わり ます。もうだめです。相撲のアナウンサーが一瞬にして「左四つになりました」 とか言うのは驚嘆するしかありません。

  左右で一番くやしかったのは小学校の入学試験のときです。えーと福島大学教 育学部付属小学校です。父が当時福島大学の助教授だったので実質フリーパス だったのですがもちろん受験する必要はありました。出された問題の一つが10 個くらい並んだ棒を先生が指さして「これは左から何番目？」とかいうもので した。左から3番目に置いてあったのは今でも覚えています。左というのもお箸 方式で分かりました。

  ところが「左から」というのが自分から見てなのか、先生から見てなのかが分 からなかった。そして当時はそれを質問する言語を持っていなかった。結局の ところ発したのは次の言葉です。

  分かりません。

  ああ。情けないやら悔しいやら。まあフリーパスだったからいいんですけど。 もっともフリーパスで付属小学校に入りエスカレーターで付属中学校に入った 影響で、つねにクラスで一番おばかというつまんない小中学校生活を送りまし た。高校と大学は実力で入りました。たぶん。

  コメント

  _ふちの [あ、これとても共感できます。ちなみに僕は左ききなのでお箸を持つ手は左です。ドライ...]

  _かがみ [ふちのさん、こんにちは。左右が分かりにくいのは本当に不便で、例えば知らない道でコ...]

  _ふちの [僕の場合 non-verbal には左右の違いは分かっているので、道がわからなく...]

  _かがみ [あ。失礼いたしました。私は自分が運転していて横の人に「次の角を右に」と言われても...]

  _標準モデル [右剰余類と左剰余類は別の意味で混同しやすくて困りますよね。鈴木通夫「群論」とか原...]

  _かがみ [右加群、左加群は分かりやすいのに右剰余類と左剰余類は分かりにくいです。にしてもこ...]

• PRS-600使ってみた (続き)

  PRS-600 でのPDF閲覧については下の記事に書いたように横のマージンがなかなか小さく ならないのが少々困るところです。普通にできる最適化としては次の方法です。

  1. Preview の「プリント」の「用紙サイズ」の部分に縦横比が 4:3 (これは PRS-600 の 800x600 ピクセルに対応しています) の「用紙を定義する」例えば 16cm x 12cm で良いです。また上下左右のマージンをすべて 0 と定義します。
  2. この状態で「サイズ調整」を行い上下がはみ出ない限界までサイズを大きくする。
  3. PDF ファイルに対しての印刷を行う (左下の PDF ▼)

  これが通常の方法でできる最良の方法であると思われます。もし上下のマージ ンが非常に大きい文書であれば、上記方法で横方向のマージンを限りなく 0 に 近づけることが可能です。その場合 PRS-600 でもほとんど横マージンなしで文 書を閲覧することが可能です。残念ながら通常文書の性質と、さらに文書の縦 横比と PRS-600 の縦横比の関係もあり縦方向が先にはみだしてしまう場合がほ とんどです。それでも大分改善され明るいところでのランドスケープモードな らば十分読めるようになりました。

  もっと欲張るならば一ページの縦方向を「わざとはみださせて」ページ分割さ せれば良いのですが、Acrobat ならば可能なのかも知れませんが、Preview で は無理なようです。そのような機能をもつフリーソフトは見つかりませんでし た。PostScript 経由で上記のようなページ分割が可能であるとうれしいのでぼ ちぼち探してみます。ご存知の方がおられたら教えていただけるとうれしいで す。

  コメント

• PRS-600使ってみた

  PRS-600 を少し使ってみたので感想を。いくつか批判的なことも書きますが非常 に気に入っています。ここがもう少々改善されたらうれしいなということで。

  昼間不在だったわけでもないのになぜか昨日の夜の21時頃配送されました。思っ たより箱が小さくてびっくりです。中身を取り出すと画面の大きさが iPhone の丁度2倍程度という感じです。USB 経由で MacBook に接続すると自動的に2つ のヴォリュームがマウントされます。Launcher という名前のヴォリュームと Reader という名前のヴォリュームです。Launcher にはホスト PC で使うソフ トウエアーが入っています。Reader が書籍等のデーターを格納するヴォリュー ムであると思われます。

  さっそく添付されていた eBook Library というソフトをインストールしたので すが、なんとソフトウエアーが PRS-600 を認識しません。素直に Windows で 処理を行えば良いのですが、早く一冊でも本を読みたいという欲望に勝てません。

  ところで Reader ヴォリュームの中を調べると /detabase/media/books/ とい うフォルダーが存在します。試しにそこに一冊 PDF 本をコピーしたところうま いこと本体で読めるようになりました。

  文字ががちっちゃいです。

  これはもしかして老眼の人は使えないのではとちょっとがっかりしました。最 初のデフォルトはポートレートモードだったので試しにランドスケープモード に変更しました。このモードだとなんとか読めるようです。それでも少々苦し いです。実はフォントを大きくするオプションがありそれに期待したのですが、 PDF の場合最小の拡大率でも2倍に拡大され、さらに埋め込みフォントの場合拡 大されない、最悪文字化けする状態で、この機能は使えませんでした。フォン トの拡大とは別にズームモードというのがあり、これは自分の好きな大きさま で文字を拡大することが可能でとても使い勝手が良いです。

  ところがズームモードは一ページ分しか有効ではなく他のページに移行した場 合ズームモードはキャンセルされ、同じ倍率にズームするために何回も同じ操 作することになります。

  フォント拡大モードと同様な感覚でズームモードが使用可能であれば完璧であっ たと思われます。実際 B5 版の本と画面の大きさを比較すると、あと 20% 文字 が大きければ本とほとんど同じ大きさのフォントで読むことが可能と思われる のです。ランドスケープモードの場合ページとしては上下分割されるわけでそ れほど厳密にもとのままである必要もなさそうなので、左右マージンぎりぎり モードがあると良いと思います。

  左右のマージンといえば PRS-600 は書籍の体裁に忠実ということでかなりマー ジンを大きくとっている感じがします。書籍自体のマージン+αという感じです。 たしかにマージンが極端に少ない書籍は余り見栄えが良くありませんが、小さ めの電子機器での閲覧となればマージンよりも字の大きさの方が大切です。

  (秘伝) まずプレヴューで転送したい PDF 文書を開きます。そうして上下がは みでない要に注意して横がぎりぎり紙の外へでないような拡大で PDF としての 印刷を行うのです。左右より上下のマージンが少ない場合が多いので余り拡大 率を大きく出来ないのが難点ですが、特に上下左右ともマージンが大きい文書 についてかなり改善されます。

  もっともろくに内容を読まないで文字が小さくてズームが不便だと言ってるの が悪いわけで、真面目に読むとなれば一ページを読むのにそれ相当の時間をか けるので特に無理する必要はないのかも知れません。

  最初「これはけしからん」と思ったのはランドスケープモードで上下の文字の コントラストが非常に弱くなりかすれて見える場合があることです。場所的に はポートレートの余白部分なので表示機器のてぬきかとさえ思いました。とこ ろがよくよく見るとランドスケープにおける下部のかすれたところは「次のペー ジ」先頭ではっきり見える。上部のかすれたところは「前ページ」でよく見え る。ページ変更で3行分くらい重複するのですが、ここは重複していますという ことがはっきり分かります。でなかなか面白い工夫だなあと思いました。

  以上いくつか批判的なことも書きましたが非常に気に入っています。

  (後日談) 基本的にフォルダー間のファイルコピーで PDF 文書は読めるように なるのですが、eBook Library の機能を使わないと文書のテーマごとの振り分 けができません。eBook Library は Snow Leopard 32bit kernel では動作する そうですので、ここは時が経つのを待つことにして MacBook を 32bit kernel に 戻しました。戻し方は簡単でした。

  # bless --folder /System/Library/CoreServices --file /System/Library/CoreServices/boot.efi
  

  ここのところはいざという時のために 64bit ブートパッチの EFI とオリジナ ルのを区別しといたのが大正解でした。

  (さらに後日談) 私の指が太いせいか画面の反応がいまいちよろしくありません。 PRS-600 はペンタッチもサポートしています。ただし標準のペンは梱包されて おらず、マニュアルに鉛筆やボールペンは使わないで下さいと書いてあります。 ためしに綿棒でタッチしたら非常に反応が良く快適です。手書きモードでも使 えそうです。綿棒ならいくらなくしても大丈夫。なかなか良い道具を発見しま した。

  (さらに) なんか MacBoook の eBook Library が起動しなくなりました。Sony はソフトウエアーに関してはだめですね。というわけで使う頻度は少なそうな ので書類の整理のみは自宅の Windows マシンで行うことにしました。

  コメント

  _通りすがりさん [電子ブックリーダーには興味があるのですが、いかんせん電子ブック自体がほとんど流通...]

  _かがみ [通りすがりさんこんにちは。コメントありがとうございます。電子ブックというより手持...]

• PRS-600届く

  本日 PRS-600 が届きました。レヴューは後日。

  コメント

• 日曜日の日記

  今日も仕事でした。でも合間に Haskell のインストールとか遊んでしまいまし た。秘策があるのかいまいち分からないのですが、現在のところ Snow Leopard で Haskell の ghc コンパイラーは動作しないようです。なので当面 Parallels 上で動く FreeBSD の中の Haskell で遊ぶことにしました。この二 三年コンピューターに全く興味がなくなり、一応これで食べているので困った ものでしたがSnow Leopard kernel 64bit 化作戦あたりから興味が戻ってきた のかも知れません。数学の方にも良い影響がでることを期待しています。

  奥さまのメールボックスにレンタルサーバー (www.inetd.co.jp) から大量のメー ルが。たまにすりぬけるスパムメールが奥さまのイーモバイルに転送されて、 イーモバイルの怒りが爆発し、レンタルサーバーのアドレスをスパム送信ホス ト情報データーベース (http://www.fortiguardcenter.com/) に登録したよう です。陰険ですな。さらに MAILER-DAEMON からのメールを再び転送するような 甘い設定だったのでループ状態になったようです。レンタルサーバーに大変な 迷惑をかけてしまいました。自分のスパム学習はそれなりまめに行っていまし たが、奥さまの方を最近全然メンテナンスしていないのが悪かったようです。 とはいえスパムの転送を完全に防ぐことは非常に困難です。なので少々遅延が 増えるのが難点ですが、一度 Google Mail に転送し、そちらから奥さまのイー モバイル端末へ転送するように変更しました。ループを防ぐ設定にしたのはも ちろんです。

  最初誰か他の人がスパムメールを大量に送出したのが原因でブラックリストに 載ってしまったのかと思い、レンタルサーバーに連絡したのですが、よもや自 分が犯人だったとは。うかつでした。レンタルサーバーの対応はいつものよう に非常に的確かつ丁寧で好感がもてるものでした。

  渕野さんの「春日井日記」の URL が変更になりました。新しいアドレスは

  http://kurt.scitec.kobe-u.ac.jp/~fuchino/kasugai.html

  です。今後更新はこちらに反映されるそうです。上のほうのリンクも修正しま した。

  コメント

• 土曜日の日記

  今日は昼間中寝ていました。夜中中仕事していました。つまんなくてすみません。

  コメント

• MacBook 64bit 化作戦

  私が使っている MacBook (いわゆる銀マック) はハード的には最新の MacBook Pro と同等であるにも関わらず、Apple の「Pro じゃあなくては人じゃあない」 政策により32bit kernel しか起動しない仕様です。これで不便とか遅いという わけではありませんが不愉快です。不愉快というよりくやしいです。ところが ネットを調べるとちょっとしたパッチで 64bit kernel を起動する方法がある ようです。もちろんこのような作業はちゃんとした復旧環境が存在するところ で行うべきであり、間違っても出張先のホテルなんかで行ってはいけません。 行ってはいけませんがなんとなくひまなのでやっちゃいました。参考にした URL は Is Your Machine Good Enough for Snow Leopard K64? です。ほとんど翻訳ですが作業内容をメモします。まず /Library/Preferences/SystemConfiguration/com.apple.Boot.plist に次の行を追加します。

  <dict>
  	<key>Kernel</key>
  	<string>mach_kernel</string>
  	<key>Kernel Flags</key>
  	<string>arch=x86_64</string>  ← これ
  </dict>
  

  そして /System/Library/CoreServices/boot.efi にパッチを入れるのですが 直接直すのは危険なのでまず自分のホームディレクトリー以下に例えば boot-k64.efi という名前でコピーします。

  $ cp /System/Library/CoreServices/boot.efi ./boot-k64.efi
  

  念のため

  $ shasum boot-k64.efi
  2fb9fc10e5b4bb06f62c38b01bd9836a433897f8    boot-k64.efi
  

  そして MacBook の場合 0x266e8 番地を 0x00 から 0x04 に変更します。

  (オリジナル)
  0x266e0: 38 47 01 00  00 00 00 00  00 00 00 00  00 00 00 00
  (変更後)
  0x266e0: 38 47 01 00  00 00 00 00  04 00 00 00  00 00 00 00
  
  $ shasum boot-k64.efi
  1bf0f332e2721e22e781d171125edeb7264257a7  boot-k64.efi
  

  root に昇格して次のコマンド群を入力します。

  # cp boot-k64.efi /System/Library/CoreServices/
  # cd /System/Library/CoreServices/
  # chown root:wheel boot-k64.efi
  # chflags uchg boot-k64.efi
  # bless --folder /System/Library/CoreServices --file /System/Library/CoreServices/boot-k64.efi
  

  bless コマンドはシステムに boot.efi に対応するものを教えるコマンドみた いです。こんな危険なことして大丈夫なのでしょうか。でもここまでくると 64bitカーネルの欲望を抑えることは不可能です。リブートしました。

  とっても長い時間「起動時の待ってね」画面が表示され続けました。

  無限とも思える2分間。でもちゃんと起動しました。やれやれ。プロセスタスク を見るとちゃんと 64bit カーネルが起動しているようです。速度の違いですか？ もちろん分かりません。こういうのは心理的な要因が大切なのです。この日記 をアップロード出来る程度には安定して動いているようです。そもそも Pro な 人もデフォルトでは 32bit 起動みたいなのですが、実際に Pro を使っている 人はどうしているのでしょうか。その辺りを教えていただければうれしいです。

  コメント

• 台風とかつくばとか

  つくばは台風の進路をはずれたようで、朝方まで風雨が強かったのですが現在 (AM 11:00) はやや風が強いものの晴れ間も見えます。とはいえ都心の電車が壊 滅状態のようなので、昨日こちらに移動したのは正解だったようです。会議は 午後1時開始です。実は同じお客様と午前中に打ち合わせのグループもあった のですが、本日こちらに来る予定を立ててたので全滅みたいです。会議中止で すか。いいなあと言ったら夕方の５時に延期になったそうな。かわいそうに。

  奥さまからのメールによるとモカちゃんは「台風休校」を期待してたら休校に ならずに大変落胆したそうな。ところが直後「インフルエンザ休校」しかも12 日までという連絡が入りとても喜んでいたそうな。常々「休校の時インフルエ ンザに罹ってたら休校の意味が全くない。私は絶対に罹らない。」と強い決意 を表明していました。たしかに罹っていません。親の目から見ても意志が強い 子だなと思います。

  コメント

• 昨日のこと

  ちょっと昨日は弱気になっていたかも知れません。昨日のコメントにも書きま したが、自分の能力の限界であれば、今まで勉強したことを整理して、それな り分かりやすい入門書 (PDF) を書きたいと考えています。とはいえ本当はもう 少しなんとかなるのではという邪念もあります。今月は全然時間がとれないの で来月から fine structure の勉強を始めて目処をつけたいと考えています。 数学が好きなんです。

  明日の午後からつくばで打ち合わせなのですが、台風で行けなくなると困るの で今晩からつくばに泊まります。明日泊まるとこなして帰ってこれないのと悲 しいので明日の分のホテルも予約しました。

  コメント

• 本当のことを言うと

  もうこれ以上集合論だめな気がします。仕事が強烈に忙しいせいだと良いので すが、明らかに前に比べて頭が働かないです。でももう一頑張りしたいなあ。 とりあえず仕事ですね。

  コメント

  _てなさく [くれぐれも自分の首を絞めない方向でゆっくりやってください。]

  _かがみ [ご心配ばかりおかけしてすみません。ちょっと弱気になっているかも知れません。どちら...]

• 存在記号について

  Twitter (現在閲覧時間縮小中) で 「 のとき を満たす を取る。」というのが分からなくて困っていた時期があると書きました。すぐ にはやしさんから、存外自明と思って余り考えずに使っている人が多いのでは ないかというつっこみがありました。せっかくなので上記を正当化する論法に ついて自分の知っていることを記載したいと思います。

  (ブルバキの場合) これは簡単です。ブルバキの場合論理式 に対し は対象式。そして は の省略記法です。したがって が証明可能であればそれは が証明可能 (同じことを言ってる) なので として を「取れば」良いのです。

  (一時的に言語と理論を拡張する方法) 今注目している言語と理論に対して という定数を追加して を公理として追加します。その理論で を含まない論理式 が証明されたとします。このとき はもとの理論で証明可能であることが論理式の個数による帰納法で証明できま す。これはブルバキ以外の体系に接したとき困りに困って自分で考えた方法で す。正しいと思います。たぶん。

  (定義可能な対象式を省略記号とみなす方法) この方法は [1] で知りました。 簡単のために空集合 を考えます。そもそも空集合という「対象式」なんて存在するのでしょうか。 空集合は例えば という論理式で「定義」されます。 ( は「ただ一つ存在する」という意味です)

  ところで実際に数学を展開するとき空集合や一般に対象式がが単独で現れるこ とはありません。必ず論理式の文脈の中に現れます。例えば「空でない順序数 は空集合を要素とする」という論理式があったとします。雰囲気としては次の ような論理式になります。 は順序数を表すということで。

  

  そしてたとえば の部分は と置換します。同様に の部分は で置換します。真面目に考えると上記置換を行った論理式が期待したものであ ることが分かります。この方式の場合単に存在が証明された場合の正当性はど うするのだろう。分からない。なにかうまい方法があるのか教えて頂けるとう れしいです。というか全体的に見当違いのことを書いているかも知れません。 そのような場合もご指摘を頂けるとうれしいです。

  (追記) 最後の場合個別に ! を除去すると違う対象を表してしまうので困りま す。まとめてなんとかする方法があるのだろうか？ 分からない。

  (追記の追記) 一気に と置換すれば一般の場合も良さそう。たぶん。

  [1] Kenneth Kunen, Set Theory, An Introduction to Independence Proofs, Studies in Logic and the Foundations of Mathematics, North-Holland, 1980.

  (邦訳) ケネス キューネン著, 藤田 博司訳. 集合論—独立性証明への案内. 日 本評論社, 2008.

  コメント

  _かがみ [冷静に考えると最後のは存在記号を除去できていない。うーん。二番目の方法しかないの...]

  _平井洋一 [自然演繹で暮らしていると、「∃の除去則じゃん」と思って通り過ぎそうになるのです。...]

  _かがみ [平井さんこんにちは。コメントありがとうございます。恥ずかしいことに自然演繹のこと...]

• 仕事してます

  仕事しています。ところでお昼ご飯を食べようとしたらお金がないのに気がつ いてキャッシュなんとかからお金を下ろしました。時間外手数料105円損しまし た。それはそうと105円という大金を徴収した上、画面上に「ネットでかんたん お取引き。今申し込まれますか。」とかいうメッセージが。お金を徴収してコ マーシャルを見せるとは、さすが銀行さまは偉いです。ところで PC 上で取引 して何の利益があるのだろう。どうせ別銀行へお金を移動とかいう場合手数料 取るのだろうから、直接下ろしてから別の銀行へ入金すれば良い気ようながし ます。例えばスキャナで読んだお札がネット経由で入金可能とか、預金を下ろ した場合、プリンターに「本物の」お金が印刷されて出てくるというならば便 利だと思います。調査したわけでないので確実ではありませんが、そのような 機能は存在しないと思われます。なので却下です。

  コメント

  _てなさく [てなさくは一時期、残高照会とカード口座への振り替えにネットバンキングを利用してい...]

  _ni-capo [ネットバンキングの一番の利点は、ATMに並ばなくてすむことです。早く手続きしたい...]

  _たかたに [散財常習犯としましては、あやしげな店舗での通販ではカードを使いたくないので銀行振...]

  _てなさく [残念ながら、インターネットバンキングの操作画面には萌えキャラ銀行員さまは登場しま...]

  _かがみ [(てなさくさん) 反応が遅れてすみません。たしかに萌えキャラ画面があれば申し込み...]

  _かがみ [(ni-capo さん) たしかに銀行間でお金の移動が多い場合は便利かも知れませ...]

  _かがみ [(たかたにさん) なるほどあやしげなところからの買い物の場合便利そうです。現行で...]

• 仕事

  今日は一日仕事をしていました。金曜日ですからあたりまえです。明日も一日 仕事します。来週と再来週がここ数年間で最大の修羅場になると思われます。 少しでも体力を温存する必要があるので明後日はお休みにします。

  コメント

• 雑

  最近更新が滞り気味でさらに Twitter のコピーばかりで申しわけございません。 今月いっぱいは先月以上のハードスケデュールで余り更新できないと思います。 余りにハードスケデュールなのでまことに不本意ですが数学の方も一月封印す るかも知れません。予定としては PCF は当面断念です (残念) かなり甘く見て いたのだろうと思います。来月から fine structure の勉強をしてもしそれな り分かる部分もあった場合、その後すでに注文したモスコヴァキスの Descriptive Set Theory の改訂第2版を読みたいと考えています。前々から自 覚していたのですが、PCF でひとまず挫折して、自分は整理された教科書は読 めるが論文を読む能力はないのではと思っています。とは言えここはなんとか 克服したいところです。私は見かけによらずしぶとい面があるのです。

  いよいよ今月末に「数学ガール〜ゲーデルの不完全性定理」が出版になるよう です。結城さんがここをご覧になっているかどうかは分かりませんが、本当に お疲れさまでした。レヴューを通じ色々なことを勉強できました。充実感もあ りました。本当に楽しかったです。ありがとうございます。

  それから金欠にもかかわらず電子書籍リーダーを購入しました。米国からの輸 入なので到着するのは今月中旬頃になると思います。そちらのレヴューは実物 が届いた段階で行いたい、と思ったのですが今月の中旬はハードスケデュール の極限に達する予定なので、おそらく来月になってしまうと思います。

  てなさくさんの 10月1日の日記 は耳が痛いです。Twitter の方は少し量を減らして日記の方を少しでも充実 させたい思います。あ。でも一冊営業しました。 Red cat さんの2009年9月30日の記事 。 さらに結城さんにも一冊営業したと思われるので最低でも合計二冊です。えら いでしょ。

  コメント

  _結城浩 [結城です。こちらこそ本当に、本当にお世話になりました。現在残っている（であろう）...]

  _かがみ [結城さんこんにちは。本文にも書きましたが本当に楽しい半年間でした。今考えると勉強...]

2009年9月   2009年11月   更新履歴と日記の先頭に戻る   日記の目次 
集合論雑記目次
はてなリング 数学の輪
トップページに戻る   谷山浩子さんのページ