起床は7時、眠い。慌てて出勤。急行が蛍池に止まらないことを知らず乗り過ごして、結局5分遅刻する。 20時に退所、21時半に帰宅。夕食は牡蠣クリームシチューとマカロニ。

"Mathematics in Philosophy" pp.221-251. 新幹線内で読了・・・しかし難しい。もう一回読むことに決定。

論文の改訂が進んでいないとなじられる夢を見る。起床は11時半。実家は木造で、屋内が外よりも寒い。昼食は手巻き寿司。 実家の近所は秋の気配。もみじが赤くなってきた。 16時に東京駅へ行くも、3連休の最終日のため当然新幹線の指定はとれず、結局自由席で…

起床は11時半、乾燥していて喉が痛い。実家で一日静養。西荻窪の古本屋に行き、その後夕食、両親と鰻屋に行く。CATVで「バスカビル家の犬」（BBC／2002年版）を見て、26時に寝る。

起床は8時、安宿なのでうるさく、よく眠れず。慌てて大学へ。研究集会二日目、カリー化の話が印象に残った。ほかに自作証明系やフレーゲの話まで。面白い話が多いが、二日目なので参加者の疲労度が濃い。 大学のプレゼン室、天井の蛍光灯がデジタル数字の8の…

ホテルから更新。 起床は7時、結局５時間睡眠。あわてて空港へ行き、8時55分の便で羽田に向かう。機内で爆睡。モノレール、山手線、つくばエキスプレス経由でつくばへ。定理証明系に関する研究集会に出席する。面白い話が多い。 今回はテーマ（バランスがと…

本日よりつくばに出張し、その後実家により、関西には日曜日に帰ります。したがって、次回更新は遅ければ日曜日となる予定です。ご了承ください。

18:30-21:00、参加は三人。 Ted Siderの"Reductive Theory of Modality"を読むはずだったが、今回はK氏が、論文のネタとして考えている話と、David Lewisの謎の論証について話をする。おもしろかったが、ここで紹介するわけにはいかないので略（後者だけでも…

本日Ktさんに聞いてわかったことを、備忘のためにメモ。Agda 2 でデータ型からデータ型 への関数を定義するとき、変数の束縛に関して、思いもよらないことがおこる（昨日はバグはこのせい）。 Aのデータ型は A : Nat -> A g : (n : Nat) -> ... の形をしてお…

だんだん寒くなる。起床は9時、出勤してコード書き。様相述語論理の部分で 原始述語と and の場合の処理が完了。Not の処理で型があわず、悩む。打ち合わせ後、前勤務校の源泉徴収票を電話で送ってもらうように手配してから、17時に退所。 帰宅は21時半。夕…

午前はよく晴れ、暖かい。しかし日が暮れるととても寒い。 起床は9時、最近この時間が標準になってしまった。出勤してコード書き。型チェックに何度か失敗し、その度にKtさんに泣きつく。とりあえず、やっと、暫定的に述語論理はパスするが、今度は様相論理…

朝は暖かいが、日が暮れると急に寒くなる。画像は朝の風景。朝の光が海に反射する。 起床は9時、遅め。郵便局に寄ってから出勤。コード書き、いろいろ難航する。やはり任意の自然数nについて、コンピューター上でn変数述語を用意して述語論理を展開するのは…

昨日は水曜日読書会のまとめ記事、本日は上記書類に予想外に手間取ってしまったため、「ラッセルのパラドックス」の更新は今週はお休みさせていただきます。申し訳ありませんが、お気長にお待ちいただければ幸いです。

暖かい日。起床は12時半、よく寝た。読書と論文読み。夕食は18時、貰い物のカニのトマトソースパスタ。 カニなんて、年に何回食べられるのやら。 食後は某書類。内容はともかく、Mac上で扱うワードやエクセルとプリンターの関係でひどく苦労する。25時半まで…

読書会の記事と、木曜日の談話会の記事を追加しました。ご意見をいただければ幸いです。

よく晴れた暖かい日。起床は11時。洗濯と掃除をする。先週は夫婦そろって出張だったので、二週間分たまっている。13時にはCも実家から帰ってくる。掃除の続きと家具の配達。 夕方、Cと外出。三宮で本屋とデパートに行き、ハンバーグを食べて帰る。

急に寒くなる。起床は9時、出勤してコード書き、噂は確認がとれず。午前中の会議は機器不良のため中止、午後はH氏と認証に関して議論。夕方から某プロジェクトの打ち上げ。24時に帰宅、27時に寝る。

物理ではシミュレーションはもはや不可欠な道具だが、シミュレーションに関して 定量的な議論はできるが、定性的な議論はできない モデルの妥当性を問うことが難しい（シミュレーションが変な数字を出してきて初めて前提のおかしさに気づく） という問題があ…

今日もよく晴れる。起床は9時。出勤してコード書き。現在悩んでいる問題は、実は既にOさんの手で実装されていたらしい、という噂を聞く。ついでに、来週末もまた出張となった。午後は全体会議と談話会、19時に帰宅しようとしたところちょうど飲んでいたグル…

意気消沈すると、少し感傷的になり、ちょっとしたことで涙もろくなることもある。 先週末、東京への出発の直前、変なメールを受け取った。本文は空白、添付はpdfファイルが一つだけ。SPAMかと思ったが、帰ってきた後ファイルを開いてみた。すると「あなたの…

19時より22時まで。参加者3人。p.18第2段落より最後まで。 パットナムのトリック K氏の指摘で議論が始まる。p.19の第一パラグラフ-第二パラグラフの重要な点でパトナムは叙述トリックを使っている。 第一パラグラフでは、集合論のパラドックスの話で、ラッセ…

よく晴れた、暖かい日。起床は9時、二日続けて遅め。 出勤してコード書きの続き。打ち合わせで失敗を報告、意気消沈する。早めに退所、読書会へ。 帰宅は22時半、夕食はマカロニ入りトマトシチュー、美味。

これまで誤解していたが、Agda2のdata typeの型の定義で、 (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、 (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ ということ…

起床は9時、少し遅め。出勤してコード書き。この件で時間を取られ、メールを書いたりしなければならなかったのに結局何もできず。気がついたら20時、慌てて退所（帰宅は22時）。Cも東京から帰ってきた。

帰ってきました。発表の出来はそれなり、また多くの方とお話をすることができ、とても楽しかったです。皆さん、ありがとうございました。

東京は晴れ、久しぶりに暖かな日。 しかし大阪に来ると肌寒く、小雨が降る。 起床は10時、少し二日酔いが残る。両親と昼食、昨日の残り物（寿司+鰻の白焼き）が出る。 荷造りをして、新幹線で新大阪へ。研究所に出勤、ノートPCを置いた後、少し調べものをす…

昼のビアホールへ。今度こそ心おきなくビールを飲む。それからいろいろお話を伺う。特に直観主義に対するゲーデルの立場と、直観主義へのクライゼルの影響について。立川と武蔵境をまわり、25時に帰宅。

14時45分に集合、15時からワークショップ、提題者の一人として「包括原理と超準的自然数」という内容の発表をした。提題者4人のなかで一番最初に発表でしたが、発表の出来はそれなりと言ったところでしょうか。今回のワークショップは、出席された方が40人、…

会場が前日と変わっていて、少し遅れて到着。ワークショップに行くが、レジュメがもうなくなっていたので、残部がないかと聞いたら会場係員（ボランティアの大学生？）に睨みつけられた。レジュメがなかったせいもあってか、派手に論旨を誤解する。ついでに…

二日続いて寒い日。小雨が降り続く。起床は9時。