曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

自然演繹のここがダメ! 4選(by ジラール)

 ジャン=イヴ・ジラール先生といえば、線形論理の開発者であり、他にもさまざまな斬新な業績を打ち立てた論理学界の大巨人である。ジラール先生の線形論理解説論文"Linear Logic: Its Syntax and Semantics"に自然演繹の4つの問題点というのが書かれていた。これは線形論理の証明をどう描くかという観点からのもので、推件計算はカット除去手続きに関してチャーチ=ロッサー性を満たさないという欠点がその前に挙げられている(直観主義論理の自然演繹ではこれが起きない)。非本質的な分岐ができてしまうのである。以下の自然演繹の欠点は、基本的に推件計算は逃れている。

 あとここで挙げられているのは特にジラール先生のオリジナルというわけでなくよくある議論かもしれない。私はよく知らないので、もしそうだったらすみません。また、本文では線形論理の結合子と暫定的な規則について述べているが、ここでは線形論理に限らず広く自然演繹一般についても当てはまりそうなのでその方針で書く。

その4つとは

非対称性

 古典論理の推件計算には左辺と右辺の対称性があるが、自然演繹ではそうならない。複数の前提があっても結論は常に一つだからである。これは古典線形論理を考えるうえではちょっと良くない。となるとそもそも古典論理と自然演繹の相性が良くないということに帰着してしまう。そういう議論は証明論的意味論とかであると思う。私はよく知らないのでまたいずれ考えます。

実際の数学との違い

 除去規則の問題点である。例えば「AならばB」と「A」に"ならば"除去を適用すると「B」が出てくるが、これは上下が逆なのではないか、ということらしい。これはちょっとよくわからなかったが、ふつう数学をやる際は「B」を証明したいという動機から「AならばB」と「A」を証明するのではないか、ということかと思う(たぶん)。ただ、ジラール先生も書いているがこの点はそれほど本質的な批判ではない。しかしやはり証明論的意味論とかではもんだいになるかも(証明論的意味論をよく知らないのにイメージでいろいろ言ってすみません)。

グローバルな性質

 "ならば"導入則や"または"除去則などの問題点である。これらの規則は適用する際にそこまでで出現している仮定をすべて消去しなければならない。これはなかなかややこしい。直前の式だけでなく証明図の全体を参照しなければならないのである。"This global character of the rule is quite a serious defect." とジラール先生も書いている。

余計な論理式

 "または"の除去則と存在量化の除去則で出てくる問題である。規則が適用される"または"や存在量化子を含んだ論理式とはまったく関係ない論理式が帰結として出てきてしまう。これはなんか変な感じがする。

 また、この性質のせいで(らしい)"permutation conversion"とか"commutative conversion"と呼ばれるものを考える必要が出てきて正規化が非常にややこしいものになってしまう。

証明ネットへ

 これらの欠点を逃れ、尚且つ推件計算の欠点も免れているものとしてジラール先生が提案するのが((乗法的)線形論理についてだが)証明ネットである。ただしこれは証明の体系ではないっぽい。あくまで片側推件計算の導出(証明)をグラフに置き換えて構造を単純化する装置で、証明ネットの規則にしたがって生成されるグラフは一般的に導出(証明)になっていない。

 まあ大変である。

 

↓表紙に証明ネットが描かれてる。