5日前の記事「自然演繹はちっとも自然じゃない -- 圏論による再考」において、次のように書きました。
自然演繹に対する再考は出来たと思います。でも、再構築には至っていません。
...[snip]...
いずれ別記事としてストリング図と多圏を準備した上で、自然演繹の再構築ができたらいいな、と思っています。
目論見としては出来ると思ってます。が、実際に遂行する気力が続くか？ はまた別な問題です。自然演繹の再構築に何が必要かは見当がついているので、それについて書いておきます。
まず、セマンティクスとしては多圏（polycategory）を使いたい -- 長年、言及するだけで定義も構成も不十分という状態なので、多圏をちゃんと構成したいですね。
モノイド圏Cから、対応する多圏Poly(C)を構成するのですが、いきなり多圏は難しいです。準備として、Cから別なモノイド圏Spid(C)を作ります。Spid(C)はモノイド圏Cのスパイダー圏と呼んでいるものです。
もとのモノイド圏Cとそのスパイダー圏（これもモノイド圏）Spid(C)の関係を調べるには、モノイド関手、モノイド自然変換、モノイド同値などの道具を揃える必要があります。また、モノイド圏における一般化された結合律や単位律も使います。ここらは、モノイド圏の一般論に関する準備となります。
スパイダー圏Spid(C)が構成できて、その基本性質が明らかになれば、多圏Poly(C)の構成は容易です。もとのモノイド圏Cが対称なら、Poly(C)にも対称性を持ち込めるし、Cが対称でなくてもPoly(C)は作れます。
セマンティック駆動の立場では、圏／多圏を作っておいて後から構文構造である形式的体系を作ります。したがって、形式的体系は一意には決まりません。推論規則や公理の選び方には恣意性がある、ということです。とはいえ、何かを選んで形式的体系（演繹系、論理システム）を組み立てる必要があります。複数の形式的体系を作ってもいいかも知れません。
今まで述べた手順をまとめると：
- モノイド圏の一般論の準備
- モノイド同値 →「モノイド自然変換とモノイド同値関手」
- モノイド圏が作る2-圏
- マックレーンの一貫性定理 →「ツリー書き換え系とマックレーンの一貫性定理」
- モノイド圏からのスパイダー圏の構成
- モノイド圏からの多圏の構成
- 形式的体系の構成
これらの大項目をさらに細分する必要があるかも知れません*1が、項目を実行した記事が書けたら、ここからリンクを張ることにします。
*1:[追記 date="2016-07-20"]実際に、1番目を細分しました。[/追記]
