論理や型理論では、「推論」、「判断」、「証明」、「導出」なんて言葉が出てきますが、用語法が錯綜していて、それらの言葉が何を意味するかよく分からない事態が生じます。抽象化された構造を準備しておいて、それを参照枠にすると、多少はマシになるでしょう。
抽象化された構造として、演繹系〈{deductive | deduction} system〉について述べます。演繹系とは、自由オペラッド〈自由複圏〉の生成系のことです。$`\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{－}}
\newcommand{\Iff}{\Leftrightarrow}
`$
内容：
オペラッド
オペラッド〈operad〉については、過去に何度か話題にしています。「デカルト閉圏、複圏、多圏、パッキングとカリー化」の最初の2節を読めばだいたいの感じはつかめるでしょう。より詳しいことは「モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 」に書いてあります。ブログ内の検索結果は：
「オペラッド」と「複圏〈multicategory〉」は同義語です。用語の対応は次のようになります。
| オペラッド | 複圏 |
| 色 | 対象 |
| オペレーション、オペレータ | 複射〈multimorphism〉 |
圏と複圏〈オペラッド〉の記法を揃えるなら、$`\cat{M}`$ を複圏として：
- 対象の集合 ： $`|\cat{M}| = \mrm{Obj}(\cat{M})`$
- 複ホムセット ： $`\cat{M}( (A_1, \cdots, A_n), B)`$
- 複射のプロファイル：
$`\quad f:(A_1, \cdots, A_n)\to B \In \cat{M}\\ \Iff f\in \cat{M}( (A_1, \cdots, A_n), B)`$
オペラッド〈複圏〉における結合〈composition〉は、次の2つの形が使われます。
- オペレーションのリストと単一のオペレーションの結合： $`g\circ(f_1, \cdots, f_n) = (f_1, \cdots, f_n) ; g`$
- 単一のオペレーションと単一のオペレーションの結合： $`g \circ_k f = f ;_k g`$
「オペラッド」が、単一対象の複圏を意味することがあります。そのときは、単一対象とは限らない複圏を色付きオペラッド〈{colored | coloured} operad〉と呼びます。単一対象であることを強調したいなら色無しオペラッド〈{uncolored | uncoloured} operad〉と言いますが、これは単色オペラッドと言うべきでしょう。
生成系と自由オペラッド
集合 $`C`$ を固定します。オペラッドの用語法だと、$`C`$ は色の集合〈set of {colors | colours}〉です。さらに次のような構成素〈constituent〉達を考えます。
- 集合 $`G`$
- 写像 $`\mrm{src}: G \to \mrm{List}(C)`$
- 写像 $`\mrm{trg}: G \to C`$
これらを組み合わせた構造 $`(C, G, \mrm{src}, \mrm{trg})`$ にはいくつかの呼び名があります。
- オペラッドの生成系〈{generators | generating {set | system}} for operad〉
- 複圏の生成系〈{generators | generating {set | system}} for multicategory〉
- 複グラフ〈multigraph〉
対応して、$`C, G`$ の要素の呼び方も幾つかあります。
- 色〈{color | colour}〉と生成オペレーション〈generating operation〉
- 対象〈object〉と生成複射〈generating multimorphism〉
- 頂点〈vertex〉と複辺〈multiedge〉
グラフ〈有向グラフ〉から圏が自由生成されるのと同様に、複グラフから複圏が自由生成されます。複グラフを $`M = (C, G, \mrm{src}, \mrm{trg})`$ として、自由生成された複圏／オペラッドを $`\mrm{FreeMulticat}(M)`$／$`\mrm{FreeOperad}(M)`$ と書くことにします。
適当な生成系 $`M`$ により $`\mrm{FreeMulticat}(M)`$ と書ける複圏、あるいはそれと同型な複圏が自由複圏〈free multicateogry〉です。自由オペラッド〈free operad〉は自由複圏と同義語です。
演繹系
演繹系〈{deductive | deduction} system〉とは、自由オペラッド〈自由複圏〉の生成系のことです。ただし、出自が違うので、用語法・記法は全然違います。また、扱いやすさのために条件を付けたりもします。
オペラッドの生成系〈複グラフ〉 $`M = (C, G, \mrm{src}, \mrm{trg})`$ が次の条件を満たすときやせている〈thin〉と呼ぶことにします*1。
- $`\langle \mrm{src}, \mrm{trg}\rangle : G \to \mrm{List}(C) \times C`$ が単射である。*2
この単射による像 $`\langle \mrm{src}, \mrm{trg}\rangle(G) \subseteq \mrm{List}(C) \times C`$ と $`G`$ を同一視してしまうと、やせた生成系は次の構成素からなるとみなせます。
- 集合 $`C`$
- 部分集合 $`G\subseteq \mrm{List}(C)\times C`$
- 第一射影の制限 $`\mrm{src} = \pi_1|_G : G \to \mrm{List}(C)`$
- 第二射影の制限 $`\mrm{trg} = \pi_2|_G : G \to C`$
$`\mrm{src}, \mrm{trg}`$ は自動的に作れるので、やせた生成系は次のように書けます。
$`\quad (C, G) \text{ where } G \subseteq \mrm{List}(C)\times C`$
演繹系〈自由オペラッドの生成系〉に「やせている」という条件を付けることもありますが、これは不便なことがあるのでやめたほうがいいでしょう。
nLabの deductive system の項目を参考に、オペラッドの用語法と演繹系の用語法の対照表を作ると以下のようです。
| オペラッドの用語 | 演繹系の用語 |
|---|---|
| オペラッドの生成系 | 演繹系、推論系〈inference system〉 |
| 色 | 判断〈judgement〉 |
| 生成オペレーション | ステップ〈step〉 |
| 空リストからの生成オペレーション | 公理〈axiom〉 |
| オペレーション | 証明ツリー〈proof tree〉 |
| オペレーションのソース〈src〉 | 仮説〈hypotheses〉 |
| オペレーションのターゲット〈trg〉 | 結論〈conclusion〉 |
| 空リストから可達な色 | 定理〈theorem〉 |
この用語法で、オペラッドの色を「判断」と呼ぶのはいただけないと思います。というのも、演繹系から生成された自由オペラッド〈自由複圏〉 $`\cat{M}`$ に関して、次のような書き方をするからです。
$`\quad A_1, \cdots, A_n \vdash B\\
\Iff \cat{M}( (A_1, \cdots, A_n), B) \ne \emptyset
`$
記号 '$`\vdash`$' は、型理論の型判断や、論理のシーケントに使われる記号です。通常「判断の記号」とみなされています。ここでははメタ判断の記号なんですが、"judgement" という呼び名とメタ記号 '$`\vdash`$' の使用は混乱を誘発するだけでしょう。
ここでは、「判断」の代わりに、当たり障りのない言葉「項〈term〉」を使うことにします*3。
演繹系の例
自然演繹〈natural deduction〉（の一部）は演繹系の事例になります。
| 演繹系の用語 | 自然演繹の場合 |
|---|---|
| 項 | 論理式 |
| ステップ | 自然演繹の推論規則／図 |
| 公理 | 上段が空の推論図 |
| 証明ツリー | 自然演繹の証明図 |
| 仮説 | 証明図の上段の論理式リスト |
| 結論 | 証明図の下段の論理式リスト |
自然演繹では、含意導入のようなコンビネータも必要なので、自由生成されたオペラッドだけで完全な記述は得られません。が、基本構造の記述として演繹系を使うのはよいと思います。
シーケント計算〈sequent calculus〉（の一部）も演繹系として定式化できます。
| 演繹系の用語 | シーケント計算の場合 |
|---|---|
| 項 | シーケント |
| ステップ | シーケント計算の推論規則／図 |
| 公理 | 上段が空の推論図 |
| 証明ツリー | シーケント計算の証明図 |
| 仮説 | 証明図の上段のシーケント・リスト |
| 結論 | 証明図の下段のシーケント |
シーケント計算の詳細は置いといて、おおざっぱな構造としては演繹系とみなせます。
型理論の型推論系〈type inference system〉（の一部）も演繹系として定式化できます。
| 演繹系の用語 | 型推論系の場合 |
|---|---|
| 項 | 型判断 |
| ステップ | 型推論の基本導出規則／図 |
| 公理 | 上段が空の基本導出図 |
| 証明ツリー | 型推論の導出図 |
| 仮説 | 導出図の上段の型判断リスト |
| 結論 | 導出図の下段の型判断 |
型推論系がシーケント計算と類似なのは、演繹系としての共通性を持つからです。
おわりに
演繹系の事例として、自然演繹、シーケント計算、型推論系を挙げました。これらは、どれも（ある程度は）演繹系とみなせるという共通性を持ちます。しかし、実際にはだいぶ違うシステムです。それらの相互関係は非常に複雑です。また、演繹系とみなすことはオペラッド〈複圏〉とみなすことですが、多圏〈polycategory〉とみなすほうが自然で便利な場合も多いです（多圏については「述語論理： 様々な多圏達の分類整理」を参照）。
演繹系の利用場面は、「推論」「導出」と呼ばれるような操作を持つシステムの共通構造を粗視化して眺めたいときです。具体的な詳細や一部の構造を捨ててしまえば、演繹系の枠組みで捉えられることは多いでしょう。
