拙著紹介というか、拙研究紹介というか、最近ずっと取り組んでいる研究を紹介させていただきます。
ゲンツェンの LK についてずっと考えている、というか取り組んでいます。本先は、そのシリーズの３作目になります。
前２作については☝これらを見て頂ければ、と思います。
非常に難しい
電子書籍で出版しています。
結構長い間、もう１年くらい LK の沼にはまっています。
理解できない、というワケではなくて、考えれば考えるほど深い体系だ、という印象です。
私が LK を教えられた時は典型的な「こういうもんだ」論調で教えられたので、今振り返ると、多分、いや間違いなく、教えている側も分かっていなかったはずだ、と確信しています。
LK を通して NK のロジックを辿る
LK の推論図は、NK をメタの視点で辿るような仕組みをしており証明論(proof theory)の名に相応しいものです。
恐らく LK の推論図を説明するだけでも大学の講義半期は使うでしょう。その位、深く、難しいものだと感じます。
命題論理を辿るだけでも手一杯
φ1, …, φm →→ ψm+1, …, ψn
LK の証明を構成するシーケント(sequent)は
この形式で書かれます。
LK に手を付けた時、初めに計画していたのは、シーケントを使った問題集を出すことでした。
しかし当初の予定は大きく崩れ、シーケント（上掲記号）とはなにか？
LK の推論図ひとつひとつはなにを表すのか？
そういった問題に引き込まれてゆきました。
このためにStructural Inference-Figures, Operational Inference-Figuresひとつひとつに丁寧なコメンタリーを書きたいと思ったのです。
本３巻はOperational Inference-Figures for Propositional Logicと題されている通り、命題論理に限ってOperational Inference-Figuresを考察します。それは、かなり大変な作業でした。
機会があったら、ぜひ手に取って（電子書籍ですが）ご一読ください（英語ですが・・・）
コメント（ディスカッション）