て日々

2015年9月


2015年9月30日(水)くもり

Kunenの2009年の本(と言うたびに、どうもダジャレ中枢がムズムズするんだが、正確に言えば: Kenneth Kunen, «The Foundations of Mathematics» College Publications 2009. ISBN 978-1-904987-14-7[版元サイト] [Amazon JP])について。

この本(以下, Kunen2009)は、短かい序章を除けば全部で4つの章からなる。第I章で公理的集合論をざっとおさらいしたあと、第II章で証明論とモデル論の基本のところをやる。形式言語のシンタクスを解説し、言語に対する構造の概念を解説したあと、論理体系を導入し、証明の理論を展開する。その先にあって、この本全体の心臓部をなすのが、セクションII.12の完全性定理の証明だ。

完全性定理とは「モデル論的な正しさ」と「証明可能性」とを結びつけるいちばん基本的な結果で、「形式的体系の理論 \(\Sigma\) のすべてのモデルが同時に文 \(\varphi\) のモデルでもあるなら、\(\Sigma\) からの \(\varphi\) のフォーマルな証明が存在する」と読める。また「無矛盾な理論はモデルをもつ」と言いかえることもでき、そのおかげで、モデル理論の基本定理となっている。

そこで、Kunen2009では、完全性定理の(ヘンキン流の)証明を、たいそう丁寧に解説してくれる。たとえば、普通のテキストなら《この言語 \(\mathcal{L}\) の閉項の全体を考えます.ただし,等しいことが \(\Sigma\) から証明できる二つの閉項は同一視しちゃいましょう》と、ほんの1〜2行で済ませてしまう部分ひとつとっても、なぜ閉項を集めるのか、なぜ同一視するのか、2ページにもわたって言葉を尽くして解説してくれるのだ。

それだけではなく、Kunen2009では、論理体系も、フォーマルな証明を実際に書くことよりも、完全性定理の証明を読みやすくすることに主眼を置いて最適化されている。なにしろ、命題論理的な意味でのトートロジーは、すべて公理なのである。これは、今年度の俺の講義「数理論理学」で採用した坪井明人さんのテキストでもそうだった。論理体系のフォーマルな展開より、モデルとの対応に主眼を置くなら、たしかにこれが一番てっとり早い。

いっぽう、この論理体系で、こんどはたとえば 不完全性定理 の証明を書こうとすると、絶望的なことになる。というのも、公理が多すぎるのだ。不完全性定理の証明の核心は、与えられた記号列がフォーマルな証明であるかどうかを判定する述語を算術の言葉で書き下すところにある。当然、その前段階に与えられた記号列がフォーマルな理論の公理であるかどうか判定する述語を書く必要がある。Kunen2009や坪井本の論理体系に従って、すべての閉論理式からアトムとなるべき部分論理式を選び出しそれらの組合せパターンが命題論理の恒真式のパターンになっていることを判断する述語を算術化しなければならないなんて、考えただけで眩暈がする。そういう事情から、不完全性定理を論じた本では、公理も推論規則も最小限度に抑えたヒルベルト流の論理体系が採用されることが多い。前原昭二『数学基礎論入門』(朝倉書店)がその好例だ。

このように、目的に応じて最適化された論理体系を考えることになるわけだが、証明可能性という観点からは、それらはもちろん、互いに等価でなければならない。そうでなければそれらはそもそも「別の論理」なのであり、(われわれが古典述語論理と呼んでいる)同じひとつの論理を別様に定式化した論理体系とみなすわけにはいかない。Kunen2009の論理体系も、坪井本の論理体系も、前原本の論理体系も、あるいは現在4年生のゼミテキストに採用している高崎金久『学んでみよう! 記号論理』(日本評論社)の論理も、(古典論理に関するかぎり) 互いに等価であり、かつ、そのことは少し詳しいめに論理を勉強したことのある人間にとってはほぼ自明だ。それはいいのだが、数理論理学の初級の講義では、どれか一つのフォーマルな論理体系を選んで、それを「ザ・論理体系」として提示せねばならない。これが悩ましいところ。

著者が「この体系はフォーマルな証明を書き下すにはまるで適していないよ」とくり返し念を押しているとおり、Kunen2009の体系はそういう初学者のための「ザ・論理体系」としては不適格だ。どこが面倒だといって、フォーマルな証明には自由変数を含まない閉じた論理式という意味の「文」だけが登場することを認められているところだ。これが、フォーマルな証明を書くことを絶望的に難しくしていると、俺には思える。

そのような不便な論理体系をKunen2009が採用していることにも、もちろん理由はある。ここでは(というか、数理論理学ではほとんどどこででも)論理が「仮定の集合すなわち公理系から、定理を導出する手段」と考えられている。ところが、仮定が自由変数を含むと、証明の中でのその扱いが厄介なのだ。2年前に京都でゼミ合宿なるものを開いて数理論理学の入門講義をしたが、そのときの体系でも(とりわけ、ヒルベルト流の体系と自然演繹の体系の等価性を検証する場面で)仮定における自由変数の扱いが問題になり、@noukoknows@sho_yokoi といった熱心な受講者が議論して対策を考えてくれたのだった。だが、いまから数理論理学を勉強したいんだけど、と思っている「普通の数学徒」にとって、そういう議論は見通しを悪くする憂いがある。

完全性定理の証明が目的ならKunen2009の体系もいいし、不完全性定理の証明を目的とするなら前原本の体系がやりやすい。だが、それらがたとえば自然演繹のような扱いやすい体系と等価であることの検証は必要だと思う。実際、前原本の最初の3分の1くらいはまさにそのために費やされている。

まあ、そのようなことを常々考えているわけなので、そのことについて、俺がおとといの晩

“仮定に含まれる自由変数の扱いは厄介だけど、きちんと考えないといけないな。面倒がってKunen 2009みたいに証明図には自由変数が一切出てこないなんて論理体系を作ったら、他に皺寄せが行っちまう。”

ツイートした。そしたらそれを、神戸の菊池誠さんが見て、朝早くにこんなメールをくれた。本人の許可(と本人による推敲)を得て引用する:

哲学の岡本賢吾さんによると,Frege は自由変数が大嫌いで, 概念記法は自由変数を用いないように注意深く作られているそうです. そして,自由変数を用いないで頑張って作った論理体系に, あっさりと自由変数を復活させてしまったのが Hilbert なのだそうです. また,Frege の概念記法には推論の仮定がありません. φ を記号列とするとき,━φ という表現で φ の内容を表して, その内容が正しいと判断されたときに ┣━φ と書きます. この ┣━φ で終わりであって,┣━ の左側に仮定が置かれることはありません. 概念記法には自由変数も仮定もありません.
 もしも T ┣━φ と書く場合には,T の中に自由変数がなくても定数記号があれば, 実質的にはその定数記号は自由変数と同じ働きをします. ┣━ の左側に仮定として置かれる論理式の集合 T とは, T に含まれる定数記号についての公理的定義であると考えられます. Frege は公理的定義を妥当な定義として認めず,これが Frege と Hilbert の 考え方の大きな違いの一つでした.Frege が概念記法において自由変数を用いず, ┣━ の左側に仮定 T を置くことを認めなかったことは,公理的定義を 妥当な定義とは認めない Frege の考え方に対応するのであろうと思います.
 一般に Frege の概念記法は述語論理の祖とされています.しかし, 概念記法と述語論理は本来,全く異なるものであったのだろうと思います. 我々は現在の述語論理に慣れているので,概念記法も述語論理の視点から 理解しようとします.その場合には概念記法は,複雑で使いにくく, 充分に整理されていない述語論理の先祖であるように見えるのだと思います. しかし,もしも概念記法の考え方のもとで述語論理を見ることが出来れば, 述語論理は無節操で安易な,およそ自分の子孫であるとは言い難い 枠組みであると感じられるのかも知れません.

とまあ、なんだか斜め上のほうへ連れていかれそうなコメントなのだが、フレーゲが仮定をもたない論理に拘った理由はなんとなく想像できる。それで、自由変数のことは一旦ヨコへ置いて

コメントありがとうございます。あの、これ、まるごと今日の「て日々」に引用させてもらっていいですか?

またいつものように思いつきで好き勝手を言いますが、思うに、Frege の論理主義は「論理からすべてのことが出てくる」という論理主義だったのでしょう。公理に相当するものは、すべて論理そのものの分析から導き出されなきゃならないということなら、論理外の仮定はたしかに蛇足ですな。

と返事した。つまり「菊池誠と論理学についてのメールをやりとりした」と言いたかっただけなのだが、前置きが長すぎた。ごめん。

やるきのないあひるやるきのないあひるやるきのないあひる

先日の東京出張の旅費が返ってき(たおかげで破産を免れ)たので、おあずけになっていた 結城浩『暗号技術入門 第3版』(SBクリエイティブ)を帰り道に購入。それと、IchigoJamとパソコンの間でシリアル通信するための「USB-シリアル変換アダプタ」を ショップのふうせんの通販 で購入することに。これさえ手に入れば、IchigoJamやPanCakeを部品から自作するのだって、こちらの努力しだいで可能だ。


2015年9月29日(火)はれ

ルベーグ積分と微分との関係を論じたテキストには必ず次の定理が載っているはずだ: 実数の区間 \((a,b)\) で定義された単調増加函数は、 \((a,b)\) 上ほとんど至るところ微分可能である。ということは、何か単調増加函数 \(f\) が与えられたとき、区間上の点 \(r\) を「デタラメに」選んだとしたら、その \(r\) において \(f\) が微分可能である確率が100パーセントになる。函数 \(f\) が微分できない点が存在したとしても、石を投げたとき運悪くそのような点に石が当たる確率はゼロだ。ただしこのことは、その函数が「至るところ微分可能」であることを意味しない。こういうことが起こるところが、場合の数が無限にわたる場合の確率のわかりにくいところだが、このことは「デタラメに」選ぶということの、不思議さ、コンセプチュアルな難しさを意味している。

「デタラメさ」「ランダムさ」ということが結局のところ何であるのか、現代の確率論はうまくその問いを回避して数学として大成功を収めたわけだが、近年になって、情報理論や計算可能性理論などが、あらためてランダムネスとは何かという問いにアプローチしている。

その一環として、実数 \(r\) がcomputably randomであることとすべてのcomputable monotone functionが \(r\) において可微分となることが同値、という結果が昨年発表された(«Randomness and differentiability», by V. Brattka, J. Miller, and A. Nies, to appear in Transactions of the AMS. arXiv:1104.4465) これは、ルベーグの定理の計算可能バージョンと言える。そして、同様の結果を高次元のユークリッド空間で得たという論文が、きょうarXivで公開された: («Computable randomness and monotonicity», by Alex Galicki. arXiv:1509.07910) 俺は不覚にも昨年のBrattke, Miller & Niesの論文をチェックしておらず、今回のこのプレプリントでその存在を知った。不勉強丸出しで、お恥かしい限りである。

あー、つまり、この結果を聞いた瞬間にひそかにぴぴぴぴとアイデアが閃めいたりしたわけだが、まだいろいろ勉強しなければ迂闊なことは言えないし、それに、勉強してる間に誰かに先に解かれちゃったら悔しいし、詳しくは書かない。ルベーグ積分の勉強やりなおさなくちゃ。


2015年9月28日(月)はれ

あの本の翻訳を少しだけなりとも進めるなど。

長年慣れ親しんだJedit Xを使うのをやめてから、TeXやHTMLなどをMacで入力するのにTextWranglerを使ってきた。このエディタはガイジンさんだから、日本語の行送りや禁則への対応がダメなのだが、まあ我慢できないことはない。それは我慢したんだけど、このごろなんだか手応えが鈍重になってきた。それでまあ、こんどはCotEditorに乗りかえる。EmacsがいいとかVimがいいとか、いろいろ言われているが、これらは使いこなすまでに覚えることが多そうだ。コンソールやターミナルでViを使わないことはないのだけど。

大上丈彦さんから最新刊『ワナにはまらないベクトル行列』(技術評論社)など、本をたくさん頂戴した。ありがとうございます。

いや、たくさん頂戴した理由は、ムスメの通う中高一貫校に寄贈するためだ。いずれにせよ、ありがたいことだ。


2015年9月27日(日)はれ

中秋の名月だというので、うちの不文律にしたがって、晩飯はトンカツとなった。


2015年9月26日(土)はれ

さて困った。日記を書かねばならんのだが、どんな日だったか、何をやったか、覚えているけど、書きたくないぞ。


2015年9月25日(金)くもり

さて困った。日記を書かねばならんのだが、どんな日だったか、何をやったか、覚えてないぞ。たしか、仕事を済ませピアノのレッスンを済ませてからは、Raspberry PiにEmacsを入れたりTeXLiveを入れたり、日本語が使えるように色々といじっていたような気がする。だが、どうせ実用性はあまりない。


2015年9月24日(木)くもり

この7月末に光回線の契約をNTTからKDDIに乗り換えたこと に伴なって、ISPもSO-NETに換えた。 それまでは、10年以上の長きにわたって ASAHI-NET の世話になった。回線切り替えからそろそろ2ヶ月になるが、きょうようやくASAHI-NETの退会手続きをした。 もちろん回線が切り換わったときにすぐ退会してもよかったのだけど、 夏休み中はWiMAX2+端末を使う機会が多かったこともあって、延びのびになっていたのだ。

そういう事情で退会するのだが、ASAHI-NETは料金も手頃で、 広告のダイレクトメールもウルサクないし、WiMAX2+は出張のときとても役立ったし、 サービスに何の不満もなかった。いや本当、お世話になりました。


2015年9月23日(水・秋分の日)くもり

なんだかんだで連休最終日、秋分である。


大阪モノレール柴原駅から阪大正門への道で。
季節をあやまたず彼岸花が咲いている。

つどい2日目。あまり発表は聴かず本を読んだりエヴィン(@evinlatie)や 証蔵さん(@GLC___)とロジックの話をして過ごした。 昼食は阪大正門前のフレンドリー。土曜日に図書館で借りてちまちま読んでいたボイヤー『数学の歴史』第5版 「19世紀から20世紀まで」(朝倉書店)を、ところどころ第3版の原文と比較しながら読み終えた。 控室でうださん(@0_uda)が淹れてくれるコーヒーが、噂どおりすばらしい味だった。

月曜日には本の値段と英語の勉強の話で終わってしまったが、 ボイヤーのこの本は古代から現代までを広く浅く扱い、全体を通観させてくれるいい本だと思う。 ただし、数学そのものの解説には少し怪しいところもあるし、誤訳・不適切な訳もかなりある。

青春の像・豊中キャンパス、大高の森にて
「なんや、もう帰るんかいな。あっちにモノレール乗り場があるで。」
(大阪大学キャンパスにて)

今回は曲がりなりにも顧問らしい役目を果せたようなので、 心おきなく、運営打ち上げに参加させてもらう。打ち上げ会場は、石橋駅近くの地鶏料理の店「陽の鶏」。 参加者は証蔵さん、小泉ふゅーりー、あーく、アルゴドゥー、s.t.fake、あずあず、セシル、まれいん、加藤、ぴあのん、 俺(順不同)。出てくる鶏肉料理はどれも柔くて美味かった。夜7時から10時まで飲んだり食ったりして、阪急で梅田に移動。 23時10分梅田発の松山行き夜行高速バスに乗る。打ち上げ参加者のうち京大勢とアルゴドゥーは、 十三で河原町線に乗り換え京都に戻って、徹夜でカードゲームに興じたらしい。

《関西すうがく徒のつどい》 の顔というべき のうこ(@noukoknows)が晴れて医者になり、前回を最後につどい運営から抜けた。 今朝、千里中央から柴原に向かうモノレールで あずあず とも話したのだが、 のうこのいない「つどい」というのはなんだかノンアルコールビールみたいだ。 味も色合いも間違いなく「つどい」なのだが、何かが違う。とはいえ、そんなのは古参の繰り言にすぎない。 今回も学部生が参加者の中心であり、また、少なからぬ数の高校生の参加があったようだ。「つどい」は若い人たちのものだ。 打ち上げの席では第8回の開催を確実視させる頼もしい発言が参加者のひとりから出た。 そして のうこ の後を襲うて まれいん が新しい「つどいの顔」になっている。 ジジイの俺が心配するようなことは何もないのだ。


2015年9月22日(火・国民の休日)はれ

朝7時10分松山市駅前発のバスに乗って大阪へ。大阪大学豊中キャンパスを会場にして開催される 《第7回関西すうがく徒のつどい》 に参加する。

大阪大学豊中キャンパスにて
「どこ行くねん? ああ、理学部か。あっちや。」
(大阪大学キャンパスにて)

素数Tシャツ(@shinchan_prime)と ワヘイヘイ(@waheyhey)の発表を聴いた。 素数Tシャツの発表はZudilinの定理《\(\zeta(5)\) と \(\zeta(7)\) と \(\zeta(9)\) のうち少なくともひとつが無理数》の証明の概略と関連する予想についての話。ワヘイヘイの発表は 射影空間・代数多様体・因子の線形同値・ブローアップなど、代数幾何学の基本概念の解説で、 どちらも話題の選び方も話の運びもとても上手で、わかりやすく面白かった。「つどい」に来ると、 妬ましいほど頭の回転が早いうえ、しかもよく勉強して真摯に努力している若い人たちと、話し、 議論をして交流することができる。これは自分の奉職する大学で「先生」している時には得られない体験である。

夜食は証蔵さんと梅田地下街で和食。泊まりは心斎橋のカプセルホテル。 カプセルに泊まるのは初めてだが、フェリーの2等寝台よりはよほど広々としていた。


2015年9月21日(月・敬老の日)はれ

ムスメが部屋の模様替えをするというのでカラーボックスを5個も組み立ててやる。 昼飯に回鍋肉、晩飯に牛すじの肉じゃがを作った。どっちもうまく作れたので嬉しい。

土曜日に県立図書館で借り出したボイヤー『数学の歴史』(朝倉書店)のこと。 訳本のうち第5巻「19世紀から20世紀まで」が出版されたのは1985年。俺が大学3年生のときだ。 この訳本の原典 (Carl B.Boyer «A History of Mathematics» John Wiley&Sons)は1968年の初版だが、その後、 メルツバック(Uta C.Merzbach)の手で改訂され、最新版は2010年の第3版。 これのペーパーバック版はAmazon.co.jpで4,918円、 Kindle版なら2,407円である。訳本は第5巻だけでも3,888円する。何が言いたいかというと、つまり、 「やっぱり英語は勉強しといたほうがええぞ」と言いたい。 できれば、中学・高校で教えてもらってる間にやっときましょう。そうすれば、なんら別料金は発生しないわけだし。

念のために言うけど、俺はべつだん「グローバル人材なんちゃら」 なんていう話をしているんじゃないぞぉ〜。

というわけで、Kindle版をポチる。


2015年9月20日(日)はれ

PanCake のブレッドボード・キットを組み立て、テレビに接続して使ってみた。 IchigoJam から送ったコマンドに合わせてテレビにカラーのグラフィクスが表示されるので、なかなか楽しい。 ただ、使いこなすにはもう少し時間をかけてつき合わないとだめだし、そうなると、 ブレッドボードではちょっと頼りない。回路はとてもシンプルだし部品もどうやら手に入りやすいものばかりなので、 あとはファームウエアを書き込むツール(パソコン上の開発環境とUSBシリアル変換アダプタ) さえあれば自作も可能かと思われる。やってみようかな。

PanCake

今回のブレッドボード・キットでは黒いジャンパーケーブルが足りなかった。いやもちろん、 ジャンパーケーブルの本数自体は足りているのだが、GNDには黒色以外のケーブルを繋ぎたくないじゃないか。 FacebookのIchigoJam-FANグループでそのように感想を言ったら、製造元の方から、 各色の調達がなかなか難しいけど検討してみる、との返事を直接頂戴した。


2015年9月19日(土)はれ

セガレの小学校の運動会。 天気はよく、風がさわやかで、暑くも寒くもないという、運動会にうってつけの好天だ。 セガレの出番は障害物走(借り物競走)と騎馬戦(のウマ)とダンス。 がんばったが負けたのでくやしかったらしい。

お弁当
写真は妻が張り切って作った弁当。

そのほか、県立図書館に行って本を借り換えるなど。ボイヤー『数学の歴史』(朝倉書店)の 第5巻、稲垣良典『トマス・アクィナス「存在」(エッセ)の形而上学』(春秋社)そのほか。


2015年9月18日(金)はれ

先週の飲み会結城浩さんに頂戴した学校宛サイン色紙と、 大上丈彦さんのサイン入り『ワナにはまらない微分積分』(技術評論社)をムスメが学校に持っていった。 きょうの文化祭に出向いた妻のレポートによると、校長先生が閉会式で中1〜高3の全校生徒に色紙と本を紹介してくれたそうだ。 結城さんのメッセージ「楽しみつつ学ぼう」を敷衍し、「理系文系の分野にとらわれず、 いろんな本を読みなさい」という文脈の中で、結城さんの『数学ガール』シリーズや大上さんの本を 「ていねいに書かれたよい参考書」と推薦してくれたという。ありがたいことだ。 俺は間をとりもっただけだが、なんだか嬉しい。

Raspberry Pi をベースにしたオープンソースなノートパソコン Pi-top なるものが開発されたらしい。価格は300ドルでイギリスからの送料が50ドルだそうだ。 性能面でMacBook ProやSurfaceに(とくにストレージの容量とかで)敵わないだろうけど、 3万5千円でノートパソコンというのはけっこう魅力的だし、だいいち、いろいろ面白そうじゃないか。 …って言っても、いまはそんなことに使うお金はないのよね。

そんなことに使うお金もあんなことに使うお金もないのではあるが、 来たる火曜日・水曜日に大阪大学で開かれる「第7回関西すうがく徒のつどい」には、 運営関係者のひとりとして参加する。きょうの夕方、バスの切符を買いに松山市駅に行った。 が、前夜の夜行バスはすでに満席。仕方がないから当日朝のバスで向かうことに。 宿はカプセルホテル初体験となる予定だ。


2015年9月17日(木)くもり

職場のWindows PCをWindows 10に更新した。いまのところ使用感は悪くない、 というより、Windows 7より向上している。

iPhoneとiPadのiOSがiOS9になった。といっても、俺の使っているデバイスは iPhone5Sと第4世代iPadだから、今回のアップデートでの大きな違いはない。 なんというか、両者とも次のメジャーアップデートではターゲットから外される予感がする。

午後、妻と一緒に研修を受けていた妻の友人の みーしぇん が産気づいて入院したという報せが入った。 それで、研修後に妻が病院に様子を見にいくという。 仕事を終えて駆け付けたみーしぇんの旦那さんが上の子を迎えに行って戻るまで、妻は陣痛室でみーしぇんに付き添ったという。 で、無事出産の連絡を受けたのは帰りの車の中。なにはともあれ、めでたいめでたい。 妻の帰りが遅くなるに違いないとわかったので、今夜も俺が晩飯を担当することに。 といっても、野菜を刻んだ他は、買ってきたおかずを並べるだけ。

【翌日記】偶然にも同じ日のほぼ同じ頃に別の知人夫婦にも子どもが生まれたと、 翌日知ったのであった。それはそれは。同時多発めでたい。


2015年9月16日(水)あめ

どこかの大学の数学科の助教が「ルベーグ不可測集合の存在が選択公理と同値」と学生に伝えたという話を、 ツイッターで小耳に挟んで驚いた。それでつい熱くなってツイート連発してしまった。

その助教さんの理解は間違っていて、 ルベーグ不可測集合の存在は選択公理とは比較にならない弱い命題だ。 だが、通常の公理的集合論たとえばZFから選択公理を削除してしまうと、 ルベーグ不可測集合の存在が証明できなくなることも確かである。 「選択公理があればルベーグ不可測集合の存在を証明できる」 「選択公理がなければルベーグ不可測集合の存在を証明できない」 という二つの事実を見聞したことから「ルベーグ不可測集合の存在が選択公理と同値」 という誤解が生じたと、まあ推測できる。推測はできるが、間違いは間違いである。

このように考えれば間違いであることはハッキリするはずだ:小銭入れに32円、 札入れに1,000円あり、 それが俺の現在の所持金のすべてだとする。すると「札入れの1,000円がなければ昼メシは食えない」 「札入れの1,000円があれば昼メシは食える」ということになるが、この二つの事実を合わせても、 「昼メシの価格が1,000円であること」は導かれない。 言えるのは「昼メシの価格が33円以上1,033円以下」ということだけだ。 数学者はあんまりこういう論理的な間違いはしないものだが、ことが選択公理とか独立命題の話になると、 意外にも初歩的なポカをやってしまうものである。 これはきっと「証明できる」ことと「真である」ことを同一視する傾向が根強いからであろう。

少しフォーマルに言うと、公理系 \(\Sigma\) と論理文 \(\varphi\), \(\psi\) について、 \(\Sigma\not\vdash\psi\) かつ \(\Sigma\cup\{\varphi\}\vdash\psi\) であったからといって、必ずしも \(\Sigma\) のもとで \(\varphi\) と \(\psi\) が同値になるわけではないし、\(\Sigma\not\vdash\psi\) であることと \(\Sigma\vdash\neg\psi\) であることとは全く別のことである。 非ユークリッド幾何の発見から百数十年、「あの人のあの定理」から85年、 「コーエン革命」から50年経過しているのに、まだそうした理路が浸透せず、 「わかりやすくてかっこいい誤解」ばかりが跋扈するのは悲しいことだ。悲しいことだが、 無理解を嘆いてばかりいても仕方がない。 だって、そういう誤解を解くために適切な情報源がどれだけあるかあたりを見回してみればいい。 まったく心許ない状況だ。 数理論理学の知見をよりよく理解してもらうためには、俺たちが努力するしかない。

食材の買いもの中

仕事アンド研修のため妻が高松に泊まりこみで出かけたので、晩飯を担当する。 豚ホルモンの野菜炒めと、あとはいつもの かみなりこんにゃく に 大豆もやしの豆板醤炒め。


2015年9月15日(火)くもり

歩いて散髪に行き、コミセンの図書館にちらっと寄ってからジュンク堂書店に行き、 「炎やラーメン」で昼食をとって、アエル松山セレンディップ明屋書店もちょっと冷やかしてから大学に行ったのだが、全行程を歩いたのでけっこうくたびれた。


2015年9月14日(月)くもり

職場の同僚の多くは京都産業大学で開催されている日本数学会の会合に行っている。 俺は一足早く、普通の平日に戻った。

土曜日に注文したモニタが早くも届いている。車載用のノーブランド品で、 Amazonで1,700円という廉価なもの。サイズは4.3インチであるから、横9センチ×縦6.5センチというところ。 なにせ車載用モニタだから、電源はDC12ボルト。IchigoJam本体のようにUSB充電機で使うことはできない。 それで、仕事帰りに宮西のハードオフでジャンクのACアダプタを物色して帰る。 買ってきたアダプタのプラグを切り落してモニタの電源ケーブルに接続しなおし、 IchigoJamを起動。

10 CLS 20 PRINT CHR$(RND(256));:GOTO 20

とかなんとかいうプログラムを実行してモニタをテストする。

モニタのテストのようす

写真には、斬首されたACアダプタのプラグが写っている。 この時点では配線も導線を絡め合わせただけで、小学生の実験なみのクオリティだ。もちろん、 テストのあとでハンダつけしてテープで絶縁した。

このモニタがあれば、テレビのないとこでも IchigoJam が使えるし、今後 PanCake を使うときには、テレビに改めてPanCake の出力をつなげばいい。 BASICの真っ黒けのコンソールには関心を示さないセガレも、 PanCakeのカラフルなグラフィックスには興味をもつだろう。 IchigoJamのコンソールとPanCakeの出力が別系統に取れれば、 試しながらグラフィクスのプログラミングができるってもんである。


2015年9月13日(日)はれ

昨日アキバで購入した IchigoJam の組みたて作業。かなりひさしぶりにハンダコテを使う。

組みあがった IchigoJam のボード

テレビに接続して電源を入れると、昔なつかしい 32文字×24行のキャラクタディスプレイをもつBASICインタプリタが起動する。 俺はさっそく面白がっていじっていたが、横で見ていたセガレは 「いつになったらGUIのデスクトップが起動するんだろう」と思ったらしい。

IchigoJam の起動画面

IchigoJamのBASIC処理系バージョン0.9.xには FOR〜NEXT ループがなかったらしいが、 新しいバージョン1.0.1にはちゃんと備えられている。以下のコード

10 CLS 20 FOR I=0 TO 15 30 FOR J=0 TO 15 40 LOCATE J*2,I 50 PRINT CHR$(I*16+J); 60 NEXT 70 NEXT

を実行してキャラクタマップを表示させた結果は次のようになった。

IchigoJam のキャラクタ一覧
英数字・カタカナのほかに、いろいろの絵文字が用意されている。

やるきのないあひるやるきのないあひるやるきのないあひる

昼食は俺が担当したが、ムスメと二人で、生麺のフェットチーネを探して近くのスーパーを4軒もめぐり歩いたせいで、 昼食だかおやつだかわからない時刻になってしまった。


2015年9月12日(土)はれ

ホテルで朝食後、早めに出発。9時過ぎには秋葉原についた。 エクセルシオールカフェで一息ついてから電気店街へ。目的は IchigoJam を手に入れること。秋月電子通商で買おうかと思っていたが、あそこは11時半開店。 それまでの時間つぶしのつもりでパーツ屋さんを見て回っていたら、秋月のすぐ近くのマルツ2号店で IchigoJam のみならず Pancake も手に入ってしまった。うちの Raspberry Pi の GPIO につなぐリード線も買ったし、これでしばらく楽しめそうだ。

秋葉原で買った電子パーツなどなど

秋葉原は相変わらず賑やかだった。電気製品の店、パーツの店、 キャラクターグッズの店。髪を青く染めてコスプレでイベントのMCをするお姉さん。 メイドカフェのチラシを配る制服のお姉さん。日本語・韓国語・中国語…

(´・ω・`)の焼印が押されたケーキ
子供のお土産にキャラクターグッズの店で
ショボーン(´・ω・`)のカステラ焼を買った。

正午過ぎに東京モノ(すごくゆ)レールで羽田へ。アッパーデッキのトルコ料理で昼食。 15時の飛行機で松山に戻った。みなさんのおかげで、なんともリア充な一週間だった。感謝感謝。

そうそう。東京モノすごくゆレールで思い出したが、 朝の5時半ごろ東京近辺でけっこうな地震があって、 今朝はそれで目が覚めたのだった。


2015年9月11日(金)はれ

研究集会5日めにして千秋楽。ようやく空が晴れたので、歩いて東工大へ行く。 Sy Friedman、渕野さん、酒井くん、薄葉くんと、集合論の発表が続く。

夜には都数の合宿から戻ったばかりの たんじぇ と 修論の準備をがんばっている でんこちゃん という、物理系の学生さん2人と自由が丘で飲んできた。

ツイッターではつねに無頼派の伊達男を気取るたんじぇは、実際には優しく礼儀正しく有能で、 こう言うと本人はいやがるかもしれないがどこかぬいぐるみ的なかわいらしさをもった青年であり、 まさにいま風の理系のお兄さんである。リケジョの鑑でんこちゃんは、 量子論を勉強中ということでネコの顔を描いたTシャツを着て登場した。飾り気がなく率直で賢い。 そして実は内面的にとても強い力を持った人に違いないと、俺は思っている。 いろいろの事情で、用意した手土産があわしま堂のタルト1本しかなくなっていたので、研究集会のお開きのあと宿の近くで果物ナイフと食品ラップを買って二等分して持っていった。ごめんなさいねえ。

でんこちゃんのTシャツは、 かつてのバンド仲間のらっきょさんのお気に入りのシャツにそっくりだった。

旗の台や自由が丘の周辺は都心部とはいえまだしもノンビリした感じであり、 とくに旗の台4丁目の商店街などは、初めて来たのに、なにか懐しさすら感じさせる場所だった。 俺は(NHKのニュースとツイッターからの伝聞が主な情報源だったせいか)最近の東京にいい印象をもっていなかったのだが、少し考えを修正すべきだ。


2015年9月10日(木)あめくもり

関東の各所に水害。品川あたりはそれほどのことはなかったが、 この2日で500ミリから降った地域もあるという。 それだけの水が空の上にあるってなんだか不思議だなあ、なんて能天気な感想を持ったけど、 被災した皆様には心からお見舞い申しあげます。

研究集会4日め。Liang Yuさんの講演はランダムネスがらみで、 記述集合論との関連が濃厚でもあって、期待に違わず面白かった。 午後は田中一之先生の業績とその展開を語るスペシャルセッションだった。

夜は恵比須の銀座ライオンでかがみさん結城浩さん大上丈彦さん、俺、 というおっさんカルテットで会食。お互いの著書にサインしあったり、 寄せ書きを書いたり。とても楽しかった。このためだけでも上京した甲斐があった。

ねじ子直筆色紙
これはお宝!!
大上さんの本のイラストでおなじみの森皆ねじ子さんの直筆の色紙を
大上さん経由で頂戴した。

おっさんの寄せ書き
おっさんたちの寄せ書き。誤字は御愛嬌。
なにしろ結城さんはおばけだから写真には写らないが、
紙に想念を写すことはできる。


2015年9月9日(水)あめ

台風が来ていて、まったくひどい雨だが、こればっかりは誰が悪いわけでもない。

研究集会3日め、午前中は学術的なプログラムがなくて、事実上の空き時間。 その時間を利用して、いま請け負っている本の編集者さんに、大岡山のエクセルシオールカフェでお会いした。 若い熱血な人が現われるかと思っていたら、ほぼ同世代で話しやすかった。とはいえ、 熱血でないこともなくて、なぜこの本があるべきか、ということについて熱心に語ってくれたので、 彼ひとりのためだけにでもひと肌脱いでがんばってみようか、という心持ちになる。 まあ、上手くノセられたということかも。

午後はトリイロこと木原貴行くんの発表や哲学系の発表があって、 それからフチノさんたちのピアノ演奏があり、夜は自由が丘で懇親会、兼、田中一之先生の還暦祝いのパーティー。 田中先生はたくさんの弟子や友人に囲まれて楽しそうであった。 仙台のロジックグループを盛んにして、菊池誠(神戸の)や木原くんといった逸材を育て上げたことは、 本人の数多の学術的業績と共に、田中先生の重要な業績であると思う。

懇親会のあとは、菊池誠(神戸の)と二人で飲み直し。 彼とはほぼ同年であり、いわば細く長いつきあいである。いろいろの話をしたが、 最後にはやはり、先日亡くなった角田先生とわが恩師篠田先生のコンビの話になった。 俺はもはや、両先生の期待した形で学恩に報いることはできないだろう。だが、 なにもしないでいるわけにもいかない。彼らが思いもしなかった形にはなるだろうが、 報恩のため、そして自分自身の納得できる死にかたのために、もう少し生き伸びて、微力を尽くすとしよう。


2015年9月8日(火)あめ

研究集会2日め。雨の中、慣れない道を歩く気もしなかったので電車を利用。 東京の朝とはいえ、旗の台から大岡山まで、9時すぎの東急大井町線はガラガラであった。

いつもサスペンダーで吊ってはいているスラックス、 四六時中ゴムで引っ張られているせいで、腰のあたりの縫い目が綻んだ。 ありがたいことにJAISTの根元さんに裁縫セットをお借りできるとのことだったので、 バッグにスラックスを入れて出かけ、会場で繕いものをした。もちろんズボンをはかずに出かけたわけではない。 なにせ6泊もするわけだから、替えのズボンは持っている。

きょうは午前中に集合論の講演が二つあった。 Dilip Raghavan の基数不変量に関する発表と、 Joel Hamkins の、集合論のモデルの埋め込み写像に関する結果の発表だ。 どちらも講演者のキャラクターが強く滲み出た面白い発表だった。 インド出身の秀才 Dilip は例によってハイテンションの早口でしゃべるが、 説明が上手なのでとてもわかりやすい。かなりたくさんのことを説明しているのに、 詰め込まれているという気がしない。この話術は、できれば見習いたい。 Hamkins の発表は、集合論の研究者が結果だけ聞いたら「んなアホなことがあるわけないやんか」 と言うに違いないようなことなのだが、30分ほどして証明を聴き終わる頃には、なるほどこれは自然な結果だ、 となって、世界の見方がガラっと変わってしまっているという、ある意味とんでもない話だった。 ランダム・グラフやコンウェイ超現実数などの話題も含んでいて、実に面白かった。

午後にはあのNik Weaverの講演があった。会場に現われた Weaver は、 予想していたのとは全然違って小柄で繊細そうな人で、しかも、体調を崩しているのか、 白い大きなマスクで鼻と口を覆っている。さすがに講演のときはマスクは外していたけど、 なんだか風邪をひいているような様子で、会場にいた時間も短かかったので、直接話をする機会は得られなかった。 で、講演はどちらかというと数理哲学に近い内容であった。 モデルでの成立を意味する「validity 妥当性」でも、 フォーマルな証明の存在を意味する「provability 証明可能性」でもなく、 インフォーマルな証明があると認められるという意味の「assertibility 主張可能性」を考えることで、 それ自身の無矛盾性を矛盾なく主張できるような、ペアノ算術の無矛盾な拡張を考えられるだろう、 という話。著書 «Forcing for Mathematicians» やBSLの論説 “Set Theory and C*-algebras” (Bulletin of Symbolic Logic, vol.13 no.1, March 2007, pp.1-20) で追求した作用素環論とロジックのインターフェイスとは全然違う路線だ。まあ、 強いていえば «Forcing for Mathematicians» の最終章でこの数理哲学志向をちら見せしてくれている。 つまり彼は、作用素環論と集合論と、さらに数理哲学もやるという才人なのである。

ひさしぶりに計算理論関係の講演をいろいろ聴く機会に恵まれて、 3年前の9月の日記 に書いた問題のことを思い出した。最近この方面でいろいろの結果を出している Liang Yuさんや、 ほかならぬ Stephen Simpson先生自身が来ているのだから、 話しかけていろいろ聞いてみるに越したことはない。 YuさんやSimpson先生の知るかぎりでは、hyperdegree の minimal cover ばかりからなる錐 (cone) の存在が \(0^\sharp\) の存在を導くかどうかは未解決だそうで、Simpson先生は、 「自分はもうこの方面のことはできないが、いまだに知りたいとは思っているんだ。 できれば解いてくれ」という意味のことを言ってくれた。 Yuさんも「なるほどこれはいい問題だ」と言ってくれたし、いろいろ助言をくれた。 ただ、Yuさんが本気を出したら、きっと俺より先にこの問題を解いてしまうだろう。

明日の夜からは3夜連続で外食になるので、 きょうはセッション終了後すぐに宿に戻り、洗濯を済ませた。


2015年9月7日(月)くもり

研究集会初日。あいにくの天気だけど張り切っていってみます。

旗の台から東京工業大学大岡山キャンパスまでは歩いて20分程度。 さいわい雨は止んでいたので、スマホのナビを頼りに歩いていく。思いのほか早くついてしまったので、 準備をしているスタッフの邪魔をしないように、しばしキャンパスを散歩。

東工大の建物1 東工大の建物2
俺は古い人間だから、大学にはこういう風景が欲しい

きょう聴いた講演のなかでは、 Whitehead群についてのSteinの定理の二階算術の命題としての強さを調べたシンガポールの Yue Yang さんの講演が興味深かった。その主結果によると、\(\mathrm{WKL}_0\) 上で Stein の定理と \(\mathrm{ACA}_0\) が同値となるが、ベース理論を \(\mathrm{RCA}_0\) に弱めると、 この同値性はもはや成立せず、そこではStein の定理は強い主張とはいえない。面白いものだと思う。 Yang さんの解釈では、Whitehead群というのは「この世界の外に基をもつ自由群もどき」ということになる。 その解釈は、Yang さんの結果からは自然に出てくるものではあるが、集合論の見地からみても適切といえるだろうか。たとえば Shelah が \(\mathrm{MA}\) のもとで構成した反例は、そのように受けとれるだろうか。

なにせ、こちらは Nik Weaver の本で Whitehead の問題について勉強したばかりだし、Stein の定理は Weaver の本に書いてなかったという まさにその理由で、自分で勉強せねばならんと思っているところだ。その Nik Weaver も明日には講演をするので、もう東京に来ているはずなのだが、 きょうは会えなかった。


2015年9月6日(日)くもり

朝7時35分出発の飛行機で東京にやってきた。 明日からの CTFM2015 に出席するためだ。とはいえ、きょうは羽田から東京方面に直行するのではなく、 バスで横浜まで行ってJRに乗り換えて藤沢へ行き、 4年ぶりに かがみさんにお会いする。前回行けなかった噂のベローチェでコーヒーを飲みながらしばらく話をし、 それから小田急に乗って江ノ島へ行った。神社にお詣りしたり、大道芸を見たり、しらす丼を食ったり。 おかげで楽しい時間をすごせた。ありがたいことである。

弁天橋からみた江ノ島

夕方になって小雨が降りはじめたころ藤沢に戻って、かがみさんと分かれ、 京浜東北線と京急線を乗り継いで旗の台へ。ホテルのこぢんまりとした部屋で一息入れる。


2015年9月5日(土)くもり

午前中は涼しいめの曇り空。午後から小雨。

昼メシに冷やし中華を作った。麺を買いにちょっと離れたスーパーまで行ったのだが、 子どもらを連れていっておやつを選ばせたばっかりに妙に時間を食ってしまった。

夜になってから明日からの出張に足りないものをいろいろ思い出して、 妻に車を出してもらって大学に行ったりスーパーに行ったり。 まったくもう、自分の粗忽さがイヤになる。


2015年9月4日(金)はれ

午前中、ムスメの学校の運動会を見にいった。 若いやつらがどんなことにせよ力一杯とりくんでいるのを見るのは嬉しいものだ。

俺と妻が二人とも運動がちょっと苦手なので、ムスメも小学校以来、 運動会で楽しい思いをしたことがないというのだが、中学2年生になった今年は、 割りきって楽しめたそうだ。よかった。

ムスメの学校から大学まで歩いて、午後は普通に仕事。夕方にはまた、 ピアノ教室まで歩いた。しかもそのときは明後日からの出張に備えてふだんより沢山の荷物を背負っていた。 早めに出て、堀之内公園を通る道を選び、公園のベンチに座って本を読んだ。 いい雰囲気だが、蚊が多いのには困った。 そんなこんなで、きょうはけっこう汗をかいた。ピアノ教室からの帰り、 いつもは電車を利用するが、今回はたまたまちょうどいいバスに乗れた。 普段はこのバスはレッスンが終わる頃には出発してしまっているのだが、 たまたま遅れていたらしい。


2015年9月3日(木)くもり

Raspberry Pi をネットワークにつないでソフトウェアを更新した。基本的にDebianベースのLinuxシステムなので、扱いにはけっこう慣れている。 Free Pascal (2.6.0)をインストールしたり、環境設定ファイルをviコマンドで変更したり。

あらかじめ用意された pi ユーザのパスワードを変更し、 長年慣れ親しんだ tenasaku ユーザアカウントを別に作る。 このアカウントでシステム管理までやりたいから、sudoコマンドを使えるように権限を与える (いったん pi に戻り、sudo visudo/etc/sudoerstenasaku を書き加える。) こちとらコマンドライン平気なので、普段はコンソールにログインして作業して、 GUIは必要なときに startx で起動するスタイル。 コンソールでは日本語は文字化けして読めないから、 LANG=ja_JP.UTF-8 という設定はちょっと困る。 そこで、コンソール (TERM=linux) では LANG=C にして、それ以外の、 GUI環境の端末エミュレータ (TERM=xterm) とかOS Xのターミナルからのリモートログイン (TERM=xterm-256color) の場合に LANG=ja_JP.UTF-8 とするように ~/.profile を書く…

ひさびさにコンソール作業の楽しさを味わっている。 ただまあ、RAMが500MBでCPUが700MHzシングルコアということで、 日本語でゴリゴリと文書作成ができる環境を構築するにはちょっと苦しいかも。

現在のRaspberry Piのシステムは、Debianバージョン7のwheezyを基にしている。 (もっとも、Raspberry Pi独自にバンドルされたソフトウェアもあるので、 正式なDebianではなく、Raspbianと名乗っている。) この機会に久々にDebian公式サイトを訪れて驚いたのだが、 正式版のDebianは、現在ではバージョン8.1にまでなっているらしい。 ムスメが生まれてまもないころに、コードネームpotatoのバージョン2.2を苦労して使っていたのだが、 そのムスメがいまでは14歳。時のたつのは早いものである。


2015年9月2日(水)くもり

2年前に買って以来 ずっと放ってあったRaspberry Pi (Type B) を、 これまた2年ほど前にWindows PCが壊れて以来ほとんど使わずに放ってあった17インチのVGAモニタに繋いで使えるようになった。 これでしばらくは、お金をかけずにいろいろ遊べそうだ。 だけどイーサネットのケーブルが見当らないので、実質的な作業は明日以降。


2015年9月1日(火)あめ

いやあ、よく降った。また伊予鉄の電車が停まったよ。 まあ、今回は短時間で復旧したけどね。

8月25日の時点で Free Pascal バージョン3.0.0rc1が出たらしいので、さっそくMacBook Proにインストールするなど。

蛇足かもしれんが解説。rcというのは Release Candidate (リリース候補) という意味で、だいたいこんな感じでリリースしていいですか?とテストユーザにお伺いを立てるもの。 ベータ版よりは正式版に近い。それにしても、今度のリリースでは、DOS版のあの不具合とかあの不便な仕様とかは直っているのだろうか。