はじめに
演繹体系のひとつである「自然演繹」について、何が自然なのかについては、明確に記述されている文書は少なく思います。
フレーゲ・ラッセル・ヒルベルトらの定式化がなかなか技巧的で、人間が行う非形式的な証明における推論方法とは大きく異なることから、それとの対比として提唱された定式化が自然演繹であると私は理解しています。
ここでは自然演繹の提唱者のひとりである Jaśkowski (ヤシュコフスキー、または、ヤスコフスキー) の方法について概説します。同じく自然演繹の提唱者として有名な Gentzen のものとはやや異なる形式です。ここでは命題論理の説明にとどめ、述語論理については省きます。
なお、本記事では数理論理学の慣習にしたがって、「ならば」を $\supset$ で、「否定」を $\neg$ で表します。なお、「または」「かつ」はこの2つから導出できるので、命題はこの2つの演算子だけを使用していると仮定します。
参考文献
- Dag Prawitz. Natural Deduction. Dover Publications, Inc., 2006. (初版 1965)
仮定の導入からの推論
Jaśkowski は、人は「仮定の導入からの推論」を多用すると指摘しています。
例えば $A \supset B$ を証明するには、「$A$ を仮定して $B$ を証明」すればよいです。
また、背理法も「$A$ を仮定して矛盾を導くことにより $\neg A$ を証明する」方法なので同様であると言えます。
記法
Jaśkowski の1929年の論文では仮定の導入による文脈の区切りを箱で表しました。
次にあげるのは $(\neg A \supset \neg B) \supset (B \supset A)$ の自然演繹による証明です。※カッコ付き数字は説明のために付加しています。オリジナルの証明の書式には含まれません。
\begin{gather}
\boxed{\begin{gather}
\neg A \supset \neg B \quad \cdots(1)\\
\boxed{\begin{gather}
B \quad \cdots(2)\\
\neg A \supset \neg B \quad \cdots(3)\\
\boxed{\begin{gather}
\neg A \quad \cdots(4)\\
\neg A \supset \neg B \quad \cdots(5)\\
\neg B \quad \cdots(6)\\
B \quad \cdots(7)
\end{gather}} \\
A \quad \cdots(8)
\end{gather}} \\
B \supset A \quad \cdots(9)
\end{gather}} \\
(\neg A \supset \neg B) \supset (B \supset A) \quad \cdots(10)
\end{gather}
基本的には箱内の上部に導入した仮定 $A$ を書き、そこから導ける命題を書き連ねていきます。それにより $B$ が証明できれば箱を閉じて、$A\supset B$ をその下に書きます。
- (10) を証明するためには $\neg A \supset \neg B\cdots(1)$ を仮定して $B \supset A\cdots(9)$ を示せばよい。箱内の1段目に (10) を書く。
- (9) を示したい。そのためには、さらに $B\cdots(2)$ を仮定して $A\cdots(8)$ を示せばよい。箱を新たに開始して (2) を書く。
- (1) で導入した仮定はネストした箱の中でも使えるので、(3) として置く。つまり、(2) と (3) から (8) を示せばよい。
- (8) を背理法で示すためにその否定、$\neg A\cdots(4)$ を仮定する。これも新しい箱を作ってそこの最上段に書く。(5) は (3) からコピーしてきた。
- (4) と (5) から、modus ponens (MP) により $\neg B\cdots(6)$ が得られる。
- (7) は (2) からコピーしてきた。
- (6) と (7) は矛盾するので、背理法によって (4) の否定である (8) が証明できた。
- (2) (と (3)) から (8) が証明できたので $B \supset A\cdots(9)$ が示せた。
- (1) から (9) が証明できたので (10) が証明できた。(証明終)
たぶん本人も箱を書くのが面倒くさくなったのでしょう、1934年の論文ではインデントのようなもの (正確には数字の列) を使った書式を提案しています。
(ざっくりした) 推論ルール
- $A$ と $A\supset B$ が証明できたなら $B$ を導いてよい。
- $A$ を仮定して $B$ が証明できたなら、$A\supset B$ を導いてよい。
- $\neg A$ を仮定して $B$ と $\neg B$ が証明できたなら、$A$ を導いてよい。
以上のように比較的シンプルな規則からなりますが、これで命題論理の完全な推論体系になっているはずです (参考文献には証明はなかったが)。
まとめ
いかがでしたか? Jaśkowski のスタイルのメリットはその原理と規則がシンプルであることだと思います。一方で「ならば」「否定」にもとづく規則だけでは証明が長くなりがちだし、背理法を多用するのはあまり自然ではなさそうに見えます。
それを改善するために「かつ」「または」の演算子を導入し、それらに対する推論規則を設けて、仮定の導入・消去を証明木の形で表現すると Gentzen スタイルの自然演繹になるはずです。
以上
※誤りなどのご指摘歓迎です。