科学哲学会・論理学系セッション（10:00-12:00）
「順序数を用いないカット消去定理の証明について」（秋吉亮太氏）
非可述的な体系 のカット除去を、証明論的順序数を使用しないで行う、と言う話。可述的な体系のカット消去は理解が容易だが、非可述的な体系の場合は証明論的順序数の順序関係が複雑になる、なので、証明論的順序数を用いないでカット消去をしたい。順序数を使った帰納法のかわりに、証明図（樹）のサイズについての帰納法を使用する（そして樹の間の順序の使用は順序数の使用とほぼ同じ）。すなわち「ordinal notation-free ということであって、ordinal-freeというわけではない」。
また、この論法を適用するために、体系をBuchholzの-rule*1を使って強めてやる必要がある。拡張された体系では、証明図が整礎となり、上の論法が可能になる。元の体系の証明図は、拡張された体系への埋め込みを考えれば良い。
「非古典論理における証明論の可能性と限界」（照井一成氏）
証明論におけるカット除去は、代数的意味論においてはデデキント完備化にあたる。MV代数はどんな完備化についても閉じていない！が故に、例えばウカシエヴィッチ無限値述語論理 L はカット除去が不可能である、が、 「
Lなんて誰も使わない」が故に、たいした問題ではない。
いや、ちゃかして書きましたが、非古典論理を学ぶ人間全てが知っておくべき、非常に重要な結果だと思います。
ちなみに、照井氏の使用した「天文学者の視点（個別の論理のメタ性質を調べる）・物理学者の視点（メタ性質の外延化）」の例の元ネタがストルガツキー兄弟の「月曜日は土曜日に始まる」*2であることは、私だけが知っている。
