可以使用推论“ a，b =>¬a/¬b”的否定引入规则代替通常的“ b => a，b =>¬a/¬b”吗？

问题描述

| 我发现我在大学学到的否定引入法则使推理变得有些困惑，并认为\“ a，b =>¬a/¬b\”更有意义，因为这意味着如果b表示不正确的内容，那么b本身就是不正确的。我似乎找不到一个例子，说明通常的规则比我想使用的规则更有用。是否有理由将\“ b => a，b =>¬a/¬b\”用作规则？     

解决方法

        好的，我想我有一个非常严格的论据，可以证实所说的替换。 假设我们需要对P引入一个否定。因此，使用通常的推理规则，我们证明了 P => Q P =>¬Q 从而证明¬P。 假设如果不假定P，则无法导出Q和¬Q。但是然后从P我们可以推导出Q / \ whichQ，这将允许我们推导任何东西，包括否定重言式。 因此，我们可以通过执行以下操作来使用提议的规则证明¬P： 1. | P ... | ... 10. |问 ... | ... 20. |¬ 21. | Q / \\¬Q/ \\第10和20行的介绍 22. |¬（A => A）使用矛盾引理从第21行派生 23. P =>¬（A => A）=>第1-22行的介绍 24. A => A任何事物都暗示自己（重言式） 25.¬P¬第23和24行的介绍 因此，使用重言式，我们总是可以使用建议的推理规则。 换句话说，如果您可以使用通常的推理规则引入否定，那么您也可以使用建议的推理规则。