パースの法則

パースの法則（パースのほうそく）は哲学者であり論理学者であるチャールズ・サンダース・パースにちなむ論理学における法則である。彼の最初の命題論理の公理化において、この法則を公理に採用した。この公理は、含意と呼ばれるただひとつの結合子を持つ体系における排中律であると考えることもできる。
命題計算では、パースの法則は (("P"→"Q")→"P")→"P" のことを言う。この意味するところを書き出すと、命題"P"について、命題"Q"が存在して、「"P"ならば"Q"」から"P"が真であることが従うときには、"P"は真でなければならないとなる。とりわけ、"Q"として偽を選んだ場合には、"P"から偽が従うときは常に"P"が真であるならば、"P"は真であるとなる。
パースの法則は直観論理や中間命題論理では成立せず、演繹定理だけからでは導くことができない。
カリー＝ハワード同型対応の下では、パースの法則は継続演算子(例えばSchemeにおけるcall/cc)の型である。
歴史.
パース自身による法則の言明:
続いて、法則からただちに以下が得られることを指摘している:
注意: (("x"→"y")→"a")→"x" はトートロジーでは"ない"。しかし、["a"→"x"]→[(("x"→"y")→"a")→"x"] はトートロジーである。
パースの法則の別証明.
パースの法則を示すということは"P"→"Q"や"Q"が真であることをいうのではなく、("P"→"Q")→"P"のみを使って"P"を導くことである。"P"→("P"→"Q")を使うのでもないことに注意(後件肯定を見よ)。
"単純な証明:"
formula_1
演繹定理と組み合わせたパースの法則の使用.
パースの法則を使うと演繹定理を使って定理を証明するテクニックを強化することができる。前提 Γ の元で、命題 "Z" を導出したいとする。パースの法則を使うと、Γ に "Z"→"P" の形の前提を追加することが(コスト無しに)できる。例えば、"P"→"Z" と ("P"→"Q")→"Z" から "Z"を導きたいとする。すなわち、これに演繹定理を使った ("P"→"Z")→((("P"→"Q")→"Z")→"Z") を定理として結論したいとする。まず、前提 "Z"→"Q" を追加することができる。これと "P"→"Z" から、"P"→"Q" を得る。次に、("P"→"Q")→"Z" を大前提としたモーダスポネンスを使うことで、"Z" を得る。演繹定理を適用して、元の前提から ("Z"→"Q")→"Z" が得られたことが分かる。(("Z"→"Q")→"Z")→"Z" の形のパースの法則とモーダスポネンスにより、元の前提から "Z" が得られる。これが証明したいことであった。
含意的命題論理の完全性.
パースの法則の重要性のひとつとして、含意のみを用いる論理において排中律の置き換えとして使用できることが挙げられる。公理図式:
(ここで "P", "Q", "R" は結合子として"→"のみを含む)からは結合子として"→"のみを使った全てのトートロジーを導出できる。