直観主義論理: 証明論

筆者が気付いている範囲で、定式化が複数ありうる点に言及する。

1. 推論規則の中で、仮定を揃えるかどうか
   • 例えば、連言$\land$の導入規則(ないし右規則)には以下2つの候補がある(今回は1つ目を採用)。
   $$ \begin{prooftree} \AXC{$\Gamma\vdash\vphi$} \AXC{$\Gamma\vdash\psi$} \LL{$\small(\land I)$} \BIC{$\Gamma\vdash\vphi\land\psi$} \end{prooftree} \qquad \begin{prooftree} \AXC{$\Gamma\vdash\vphi$} \AXC{$\Gamma'\vdash\psi$} \LL{$\small(\land I)$} \BIC{$\Gamma,\Gamma'\vdash\vphi\land\psi$} \end{prooftree} $$
   • 直観主義論理では弱化・縮約が使えるので、どちらの規則を使っても同じでありそこまで気にしなくてもよい(はず)。線形論理のような部分構造論理を考える際には注意が必要である。
2. 仮定を集合とするか否か
   • $\Gamma\vdash\vphi$と書くとき、$\Gamma$を論理式の有限列(リスト)とするか、集合とするかで2つの方法がある(ただし有限列は$\Gamma::=\tuple{}\mid\Gamma,\vphi$というBNFで定まるものとする)。
   • リストとする場合は、構造規則(縮約など)を明示的に体系に入れる必要がある(今回はこちらを採用)。
   • 集合とする場合は、構造規則が持つ性質が初めから使えるので、構造規則は必要ない。より厳密には、公理を以下のように変更することで、構造規則が許容可能になる(ただしその場合、上記の1で仮定を揃える方を採用する必要がある)。
     $$ \begin{prooftree} \AXC{} \LL{$\small\text{(ax)}$} \RL{$~\small(\vphi\in\Gamma)$} \UIC{$\Gamma\vdash \vphi$} \end{prooftree} $$
3. 変数の扱い
   • 例えば、全称量化$\forall$の導入規則(ないし右規則)には以下2つの候補がある(今回は1つ目を採用)。
     $$ \begin{prooftree} \AXC{$\Gamma\vdash \vphi$} \LL{$\small(\forall I)$} \RL{$~\small(x\notin\FV(\Gamma))$} \UIC{$\Gamma\vdash \forall x.\vphi$} \end{prooftree} \qquad \begin{prooftree} \AXC{$\Gamma\vdash \vphi[x:=a]$} \LL{$\small(\forall I)$} \RL{$~\small(a\notin\FV(\Gamma,\forall x.\vphi))$} \UIC{$\Gamma\vdash \forall x.\vphi$} \end{prooftree} $$
   • 2つ目の定義の条件は、固有変数条件(eigenvariable condition) という。これは$a$が下段の判断(ないしシークエント)に出現しない新しい変数(fresh variable)であることを要求する(変数ではなく定数記号とする定義もある)。

命題論理の範囲では綺麗な対応関係があるが、述語論理になるとやや注意が必要である。というのも、1階述語論理では量化($\forall,\exists$)の範囲は1つだが、λキューブにおける依存型理論$\boldsymbol{\lambda}\mathbf{P}$では量化の範囲が任意の型になるからである。すなわち、命題を型に変換することはできるが、型はかならずしも命題に変換できるとは限らない。