■
はてなも使ってみて調子が良さそうな方を選ぶことにする．
午前中はロジックセミナーをした．読んでいる本は小野本．
プログラムの数理の教科書になっていたやつだけど，まじめに読んだことは一度もないからちょうどいい． 今日はわたしの担当で，本文からずれてcut除去定理のGentzenによる証明を与えた．
論理式Aがcutされている証明図を，より簡単な論理式Bに関するcutで置き換えていくことで証明していくという方針だ．これをやるためにcross cutと呼ばれる方法を用いる．詳細は省くが，ここで本質的に重要なのはつぎのことである：LKの推論規則がほぼすべて，上段から下段へと進むにつれ，より複雑な論理式を作るという体系になっていること．逆に言えば，証明図を上に辿れば辿るほど単純な論理式になるということだ．この「逆にたどる」ことで暴かれた，より単純な論理式に対してcutを適用し，cutされる論理式を単純化しながら証明を書き換えていく．
この方法，例えば二階論理だとそうは行かない．複雑な前提から簡潔な帰結が導かれたりするので，上の方法は破綻する．わたしは二階論理については実質的な知識はないが，それでもcut除去を示せるというのだから驚きである．
午後は勉強せずに労働した．
夜は輪講の準備をした．読んでいる本はこれ：The Book "A=B"．「超幾何級数と呼ばれるクラスに属する級数が，「閉形式」と呼ばれるcanonical formを持つかどうか」という問題は，実は一定のアルゴリズムに従って「自動的に」証明可能である，ということを述べた本．
いまはまだ本題のアルゴリズムには入っていない．わたしの担当は超幾何級数をとある標準形に変形する作業を延々とやるところだったので，どちらかというと単純労働的である．前回担当した方々が丁寧にレジュメを切ってくれていたので，助かっている．
ところで，Sageにsum((((-1)k)binomial(k,n-k)), k, n/2, oo)と入力したら，2/3sqrt(3)(-1)1/2*ncos(1/6pi + 1/6pi*n)とか答えてきたのだが，これはいったいなんなんだ．
明日は労働して，輪講のレジュメを作り終えないといけない．Urysohnの補題の証明も読みなおしたかったが，そうもいかなかった．
