可以用推理「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 

因此，使用套套邏輯，我們總是可以用推理的規則提案。換句話說，如果你可以用通常的推理規則來引入一個否定，你也可以使用推論的推理規則。