可以用推理“a，b =>¬a/¬b”的否定介绍规则代替通常的“b => a，b =>¬a/¬b”吗？

Question

我发现我在大学学到的否定引入规则有点混淆，并且认为“a，b =>¬a/¬b”更有意义，因为它意味着如果b隐含某些不真实的东西，那么b本身并不是真的。我似乎无法找到一个通用规则比我想使用的规则更有用的例子。是否有原因使用“b => a，b =>？a /？b”作为规则？

Answer 1

好的，我想我有一个非常严格的论证来验证上述替换。

比方说，我们需要引入对P的否定所以使用通常的推理规则，证明 P => Q P =>¬Q ，从而证明¬P。

假设如果没有假设P，则无法推导出Q和¬Q。但是，从P开始，我们可以导出Q/\¬Q，这将允许我们导出任何东西，包括否定重言式。

因此，我们可以做这样的事情使用规则提案证明¬P：

 
1. |P     Assumed 
... |... 
10. |Q 
... |... 
20. |¬Q 
21. |Q /\ ¬Q   /\ introduction on line 10 and 20 
22. |¬(A => A)   Derived from line 21 using contradiction lemma 
23. P => ¬(A => A)  => introduction on lines 1-22 
24. A => A    Anything implies itself (a tautology) 
25. ¬P     ¬ introduction on line 23 and 24 

因此，使用套套逻辑，我们总是可以用推理的规则提案。换句话说，如果你可以用通常的推理规则来引入一个否定，你也可以使用推论的推理规则。