アニメーションとしての証明

僕が知る限り、自然演繹（他のシステムでもいいのだが）の証明過程を証明図のアニメーションだという説明を見たことがない。証明図が静的な図形のように語っている。これはいけない、これでは本質がわからない。

計算も動的（時間的な推移）だし、証明も動的だ。アニメーションの全過程（履歴）が証明であって、個々の証明図はスナップショットに過ぎない。マー確かに、最後の証明図に途中経過は織り込まれている（木の年輪みたいな感じ）なのだが、中間で大きく変形することもある。その変形の痕跡を全部最後の証明図に織り込むのは難しい。

特に、含意導入では仮定が消えるので、消えた仮定をどう図示するかは、単に図示方法の問題としても難しい。公理と仮定だけの図をt=0（tは時間）において、t=1まで変形させた軌跡を全部考えるのが正解。t=0 は空図形だと思ってもいい。すると、真空からt=1の図形（これは結論を意味する）が生まれる過程になる。

なんかコボルディズム圏に似てるな。

計算	証明
項	証明図（スナップショット）
還元	推論＝証明図の変形
計算	証明過程
等式	メタな主張／判断

ジラール（Girard）のthe big pictureとも関係しそうだ。