皮尔士定律
（重定向自Peirce 定律）
逻辑中的皮尔士定律（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.