パースの法則（パースのほうそく）は哲学者であり論理学者であるチャールズ・サンダース・パースにちなむ論理学における法則である。彼の最初の命題論理の公理化において、この法則を公理に採用した。この公理は、含意と呼ばれるただひとつの結合子を持つ体系における排中律であると考えることもできる。
命題計算では、パースの法則は ((P→Q)→P)→P のことを言う。この意味するところを書き出すと、命題Pについて、命題Qが存在して、「PならばQ」からPが真であることが従うときには、Pは真でなければならないとなる。とりわけ、Qとして偽を選んだ場合には、Pから偽が従うときは常にPが真であるならば、Pは真であるとなる。
パースの法則は直観論理や(中間命題論理)では成立せず、演繹定理だけからでは導くことができない。
カリー＝ハワード同型対応の下では、パースの法則は継続演算子(例えばSchemeにおける(call/cc))の型である[1]。
歴史
パース自身による法則の言明:
- A fifth icon is required for the principle of excluded middle and other propositions connected with it. One of the simplest formulae of this kind is:
| {(x → y) → x} → x. |
- This is hardly axiomatical. That it is true appears as follows. It can only be false by the final consequent x being false while its antecedent (x → y) → x is true. If this is true, either its consequent, x, is true, when the whole formula would be true, or its antecedent x → y is false. But in the last case the antecedent of x → y, that is x, must be true. (Peirce, the Collected Papers 3.384).
続いて、法則からただちに以下が得られることを指摘している:
- From the formula just given, we at once get:
| {(x → y) → a} → x, |
- where the a is used in such a sense that (x → y) → a means that from (x → y) every proposition follows. With that understanding, the formula states the principle of excluded middle, that from the falsity of the denial of x follows the truth of x. (Peirce, the Collected Papers 3.384).
注意: ((x→y)→a)→x はトートロジーではない。しかし、[a→x]→[((x→y)→a)→x] はトートロジーである。
パースの法則の別証明
パースの法則を示すということはP→QやQが真であることをいうのではなく、(P→Q)→Pのみを使ってPを導くことである。P→(P→Q)を使うのでもないことに注意(後件肯定を見よ)。
単純な証明:
演繹定理と組み合わせたパースの法則の使用
パースの法則を使うと演繹定理を使って定理を証明するテクニックを強化することができる。前提 Γ の元で、命題 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→Z 1. hypothesis
- (P→Q)→Z 2. hypothesis
- Z→Q 3. hypothesis
- P 4. hypothesis
- Z 5. modus ponens using steps 4 and 1
- Q 6. modus ponens using steps 5 and 3
- P→Q 7. deduction from 4 to 6
- Z 8. modus ponens using steps 7 and 2
- Z→Q 3. hypothesis
- (Z→Q)→Z 9. deduction from 3 to 8
- ((Z→Q)→Z)→Z 10. Peirce's law
- Z 11. modus ponens using steps 9 and 10
- (P→Q)→Z 2. hypothesis
- ((P→Q)→Z)→Z 12. deduction from 2 to 11
- P→Z 1. hypothesis
- (P→Z)→((P→Q)→Z)→Z) 13. deduction from 1 to 12 QED
含意的命題論理の完全性
パースの法則の重要性のひとつとして、含意のみを用いる論理において排中律の置き換えとして使用できることが挙げられる。公理図式:
- P→(Q→P)
- (P→(Q→R))→((P→Q)→(P→R))
- ((P→Q)→P)→P
- from P and P→Q infer Q
(ここで P, Q, R は結合子として"→"のみを含む)からは結合子として"→"のみを使った全てのトートロジーを導出できる。
出典
- ^ A Formulae-as-Types Notion of Control - Griffin defines K on page 3 as an equivalent to Scheme's call/cc and then discusses its type being the equivalent of Peirce's law at the end of section 5 on page 9.
参考文献
- Peirce, C.S., "On the Algebra of Logic: A Contribution to the Philosophy of Notation", American Journal of Mathematics 7, 180–202 (1885). Reprinted, the Collected Papers of Charles Sanders Peirce 3.359–403 and the Writings of Charles S. Peirce: A Chronological Edition 5, 162–190.
- Peirce, C.S., Collected Papers of Charles Sanders Peirce, Vols. 1–6, (Charles Hartshorne) and (Paul Weiss) (eds.), Vols. 7–8, (Arthur W. Burks) (ed.), Harvard University Press, Cambridge, MA, 1931–1935, 1958.