皮爾士定律
邏輯中的皮爾士定律（Peirce's law）得名於哲學家和邏輯學家查爾斯·桑德斯·皮爾士。它被接受為他的第一個公理化命題邏輯中一個公理。這個公理是排中律的推論。
在命題演算中，皮爾士定律說的是 ((P→Q)→P)→P。 也就是說，如果你能證明 P 蘊含 Q 強制 P 是真的，則 P 必定是真的。
皮爾士定律在直覺邏輯或中間邏輯中是不成立的。在柯里-霍華德同構中，皮爾士定律是一種續體運算。
皮爾士定律的證明[編輯]
在只使用否定和蘊涵運算符的命題演算中，A ∨ B 表示為 (A → B) → B。皮爾士定律等價於 (P → Q) ∨ P 也就是 ¬P ∨ Q ∨ P ，所以它是排中律的推論。
與演繹定理一起使用皮爾士定律[編輯]
皮爾士定律允許你通過使用演繹定理來增強證明定理的技術。假設給你一組前提 Γ 而你希望從它們演繹出命題 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. 假設
- (P→Q)→Z 2. 假設
- Z→Q 3. 假設
- P 4. 假設
- Z 5. 肯定前件使用步驟 4 和 1
- Q 6. 肯定前件使用步驟 5 和 3
- P→Q 7. 演繹自 4 到 6
- Z 8. 肯定前件使用步驟 7 和 2
- Z→Q 3. 假設
- (Z→Q)→Z 9. 演繹自 3 到 8
- ((Z→Q)→Z)→Z 10. 皮爾士定律
- Z 11. 肯定前件使用步驟 9 到 10
- (P→Q)→Z 2. 假設
- ((P→Q)→Z)→Z 12. 演繹自 2 到 11
- P→Z 1. 假設
- (P→Z)→((P→Q)→Z)→Z) 13. 演繹自 1 到 12 QED
蘊涵命題演算的完備性[編輯]
皮爾士定律的重要體現在它可以在只使用蘊涵的邏輯中替代排中律(參見蘊涵命題演算)。可以從公理模式:
- P→(H→P)
- (H→(P→Q))→((H→P)→(H→Q))
- ((P→Q)→P)→P
- 從 P 和 P→Q 推出 Q
(這裡的 P,Q,R 只包含「→」作為連結詞)演繹出的句子是只使用「→」作為連結詞的所有重言式。
歷史[編輯]
下面是皮爾士自己的定律陳述:
- 第五圖像(icon)需要排中原理和與它連接的其他命題。最簡單的這種公式是:
| {(x —< y) —< x} —< x。 |
- 這是難於自明的。如下看起來它是真的。它只能在最終結論 x 是假、而它的前提 (x —< y) —< x 是真的時候是假的。如果它是真的，要麼它的結論 x 是真，這時整個公式將是真的，要麼它的前提 x —< y 是假的。但是在最後一種情況下 x —< y 的前提也就是 x 必須是真的。(Peirce, CP 3.384)。
皮爾士接着指出了這個定律的一個直接應用:
- 從剛才給出的這個公式，我們立即就得到:
| {(x —< y) —< a} —< x， |
- 這裡的 a 在 (x —< y) —< a 意味着從 (x —< y) 能得出所有命題的意義上使用的。通過這種理解，這個公式陳述了排中原理，從否認 x 為假得出 x 為真。(Peirce, CP 3.384)。
引用[編輯]
- 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.