16時から所内セミナー、Yg氏が発表。bounded arithmeticの階層 について、であることが知られている。ここで、もしであれば、が示せたことになるが、残念ながらそれも証明できないことが知られている（Paris-Wilkee）。では、無矛盾性概念をもう少し制限して…

梅雨なのに雨が降らない。初夏の日差し、さわやかな日。起床は9時半、出勤して出張の事務処理とプロジェクト関連。20時に退所、21時半に帰宅。夕食はラタテュイユのパスタ。

16時より17時半まで、出席者は10人程度。（内容については後日追加します）

雨は夜のうちに止む。よく晴れたさわやかな日。起床は9時半、出勤して書類整理、急な電話で一騒動。午後は会議と講演会。懇親会に出て、24時に帰宅。

夜、メールチェックをすると国際会議 ”Logic, Algebra and Truth Degrees (LADP 2008)” 事務局からメールがいていました。要旨がacceptされたそうです。内容は、ファジイ論理の意味の解釈についてで、ファジイ論理の真理値の意味を説明するとされる「真理の…

曇り、夕方から雨。起床は9時半、出勤して書類とメール書き。20時に退所、帰宅は21時半。夕食はラタトィユとサンドイッチ。

19時半にやっと到着。22時まで。参加者は5人、 Sg 君が初参加。今回は、前回のまとめとp.195。 先の議論から私は二つのことを引き出したいと思う。第一に、ある種の論理的必然性（分析性）の概念をわれわれは実際に持っている、ということ。そして第二に、論…

晴れ、湿度が高い。起床は9時半。出勤途中、十三駅で上司から電話を受け、急遽船津橋へ急行、上司らと合流する。某ビルで某会議、某プロジェクトについて。昼食を食べ、14時に研究所に出所。Ktさんと文案作り。18時に辞去、大学へ。 電車の車内で投稿中の論…

晴れだが雲が多い。湿度の高い日。起床は8時。関西本部に出勤、午前は健康診断を受ける。体脂肪率が21%になってしまった。雑用をしてから研究所へ。メールを書いたりして過ごす。20時に退所、21時半に帰宅。夕食はノルチアーノ・パスタ。

曇り、湿度が高い。本日はCの実家の法事。起床は9時、9時45分に車でお寺に出かけ、10時半より法事。終了後は出席者で食事に行く。その後、時差調整のため昼寝。17時に起きて、皆で焼き肉屋の「彦」に行く。20時15分に辞去、21時半に帰宅。

よく晴れる。風も涼しい。近所の男子高の体臭いらしく、一日中アナウンスがうるさい。 起床は9時、メールを書いたりBlogを書いたりする。20時にCの実家へ出発。手巻き寿司をごちそうになる。

ヨーロッパに行くときは、歯ブラシ・パジャマ・スリッパを忘れないように（湯沸かしを持ち歩くのは少しやり過ぎかもしれないが）。 風邪薬とポケットティッシュは、必要と思われる量の2倍は持っていこう イギリスの気候はわからない。

出張から帰ってきました。楽しかったですが疲れました。ついでに、時差の関係でとても眠い。 出張中の詳細については、追々加えていきます。

機内では合計3時間程度眠る。9時半に関空へ。10時半にCと待ち合わせ、三宮へ向かう。家に直行、ソファーで横になったらそのまま寝てしまう。夕食はトマトとベーコンのパスタ、22時半に寝る。 イエテボリの空港で買ったお土産のトナカイのぬいぐるみ、Ma-L。…

今日もイエテボリはよく晴れる。起床は7時、荷造りをし、朝食をとってからチェックアウト。トラムで kungsportsplatsen まで行き、空港バスに乗り込む。25分で空港到着。早めにチェクインし、お土産物を探す。 12時の便でアムステルダムへ、機内では "avatar"…

Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girard…

が19時から、jantorgtとホテルに近いので、一度部屋に戻って着替えてからと思い、ホテルに帰る。しかし、気が緩んでいたのか、八日目にして始めてトラムの路線を間違え、4駅分を歩いてホテルに駆け込む。慌ててジャケットに着替え、会場に。結局5分遅刻した。…

論文の続き。昼食は昼食は大学のカフェテリアで魚料理。食事中、D先生にMatin-Lofの '71年論文で循環性（）がその中核テーマだったので驚いた、と言った話をすると、テーブルの向こうにいたC先生がいきなり身を乗り出して来たので驚く。学者だ。C先生からHur…

起床は7時、体調は快調、空もよく晴れている。大学に行く。

英語の論文の続き。D先生からMartin-Lofの1971年論文のコピーをもらう。昼食は大学近くのレストラン、アラビアータ。なんとか食べれた。午後も続き、20時半まで。 何も食べずにホテルへ戻り、残っていた最後の風邪薬を飲み、そのまま寝る。

午前3時頃に寒気を感じて起きる。布団の上にマットを敷いてもう一回眠る。寝汗をかいて7時に起床。晴れてはいるが、少し肌寒い。昨日根を詰めたせいか、頭がフラフラし、食欲もない。とにかく大学へ向かう。

英語の論文の続き。外は明るいけれど気がついたら20時半。最後に残っていたNも帰るというので慌てて帰る。Jarntorgtの広場にあるパブで夕食。 テラスでビールを飲むにはいい気温。これで夜の21時半。熱気球も飛んでいる。 チェコビールとパスタ。

今後のAgdaの方針を決める討議、本日はUniverse Polymorphismに関して。 Agdaはご存知の通り、非常に厳格なpredicativityに基づいていますが、しかし厳格な可述性は、しばしばデータ型を定義する際の面倒の元になります。例えば record Cat: Set1 where Obj:…

開始は9時半から。 本日の講演は "A Tool for Automated Theorem Proving in Agda" (Fredrik Lindblad)のみ。定理の自動証明の効率化を図るツールをAgdaに実装する話。すみません、よく覚えていません、はい。

今日も晴れ。起床は7時、体調は良好だが咳は止まらず。 朝ご飯。バイキング形式で、シル（白身魚の酢漬け）が美味。

論文が落ちました（汗）。理由は、AIMで指摘されたのと同じく「型の変更は必然的ではない、だからそう書き直すように、ただしそうすると論旨が大きく変わるので一回落とす」（大意）（大汗）。せっかくなので、現在書いている英語版を役立てる方向で今後を検…

12時5分のトラム11番線に乗るが、遅れて来た上、トラムは行楽客で満員、危うく載り損ねる。トラムは順調に遅れ続け、 Saltholmen 駅 12:30のはずが10分遅刻。しかし、他の参加者も同じトラムに乗っていた上、フェリ−が何隻も乗り場で遅れたトラムを待ってい…

今日も雲一つない天気、気温は20度を超える。起床は8時、朝食をとって出かける。付近のスーパーでサンドイッチを探すが、ろくなものがない。結局JarnTorgtのセブンイレブンに行くが、そこも在庫一個のみ、それを買う。