シーケント計算、書き換え／正規化構造

証明は自然演繹とする。

1. 仮定と結論を持つ証明図（ペトリネット風グラフ）
2. グラフ書き換え規則としての推論規則、書き換え過程としての証明行為
3. 仮定を除く（含意導入）規則
4. 公理は仮定と考えない
5. 特殊ケースとしての仮定のない証明図
6. 非形式的なシーケント＝証明図の仕様
7. 正しい証明図とは
8. シーケントに対する証明図、命題に対する証明図
9. シーケント、命題の証明可能性
10. 推論規則がシーケント表現ではどのように書けるか？
11. シーケントを最も簡単な証明図で意味付ける
12. 証明図の書き換え規則とシーケントの（ワンステップ）推論図

正規化構造（あるいは簡約構造、書き換え構造）を持つ集合でenrichされたグラフ（圏の素材）があるとき、グラフからの自由圏／自由複圏／自由多圏にも正規化構造を入れることができて、「自由結合＋正規化」がうまくできるなら、正規な射だけからなる目的の圏を作れる、って筋書きだな。