パースの法則のソースを表示

'''パースの法則'''（パースのほうそく）は[[哲学者]]であり[[論理学者]]である[[チャールズ・サンダース・パース]]にちなむ[[論理学]]における法則である。彼の最初の[[命題論理]]の公理化において、この法則を[[公理]]に採用した。この公理は、含意と呼ばれるただひとつの結合子を持つ体系における[[排中律]]であると考えることもできる。

[[命題計算]]では、'''パースの法則'''は ((''P''→''Q'')→''P'')→''P'' のことを言う。この意味するところを書き出すと、命題''P''について、命題''Q''が存在して、「''P''ならば''Q''」から''P''が真であることが従うときには、''P''は真でなければならないとなる。とりわけ、''Q''として偽を選んだ場合には、''P''から偽が従うときは常に''P''が真であるならば、''P''は真であるとなる。

パースの法則は[[直観論理]]や[[中間論理]]では成立せず、[[演繹定理]]だけからでは導くことができない。

[[カリー＝ハワード同型対応]]の下では、パースの法則は[[継続]]演算子(例えば[[Scheme]]における[[call/cc]])の型である<ref>[http://citeseer.ist.psu.edu/griffin90formulaeastypes.html 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.</ref>。

==歴史==
パース自身による法則の言明:
: 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:
{| align="center"
 | {(''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:
{| align="center"
 | {(''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'')を使うのでもないことに注意([[後件肯定]]を見よ)。

''単純な証明:''
<math>
(p \rightarrow q) \rightarrow p \Rightarrow
\overline{p \rightarrow q} \lor p \Rightarrow
\overline{\overline p \lor q} \lor p \Rightarrow
(p \land \overline q) \lor p \Rightarrow
(p \land \overline q) \lor (p \land 1) \Rightarrow
p \land (\overline q \lor 1) \Rightarrow
p \land 1 \Rightarrow
p.
</math>

==演繹定理と組み合わせたパースの法則の使用==

パースの法則を使うと演繹定理を使って定理を証明するテクニックを強化することができる。前提 &Gamma; の元で、命題 ''Z'' を導出したいとする。パースの法則を使うと、&Gamma; に ''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'')→''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'')→''Z'' 12. deduction from 2 to 11
*(''P''→''Z'')→((''P''→''Q'')→''Z'')→''Z'') 13. deduction from 1 to 12 QED

==含意的命題論理の完全性==
{{main|en:Implicational propositional calculus}}

パースの法則の重要性のひとつとして、含意のみを用いる論理において排中律の置き換えとして使用できることが挙げられる。公理図式:
* ''P''→(''Q''→''P'')
* (''P''→(''Q''→''R''))→((''P''→''Q'')→(''P''→''R''))
* ((''P''→''Q'')→''P'')→''P''
* from ''P'' and ''P''→''Q'' infer ''Q''
(ここで ''P'', ''Q'', ''R'' は結合子として"→"のみを含む)からは結合子として"→"のみを使った全てのトートロジーを導出できる。

==出典==

<references/>

==参考文献==

{{main|Charles Sanders Peirce bibliography}}

* 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 (philosopher)|Paul Weiss]] (eds.), Vols. 7–8, [[Arthur W. Burks]] (ed.), Harvard University Press, Cambridge, MA, 1931–1935, 1958.

{{デフォルトソート:はあすのほうそく}}
[[Category:チャールズ・サンダース・パース]]
[[Category:命題論理の定理]]
[[Category:数理論理学]]
[[Category:直観主義]]
[[Category:数学に関する記事]]