判断论证¬q,p→q ⊢ ¬q是否有效及推导错误分析

我最近在判断这个命题论证的有效性：
$$ \neg q,p\to q \vdash \neg q $$
按照拒取式（Modus Tollens）的规则，从$\neg q$和$p\to q$能推出的典型结论是$\neg p$，所以我一开始误以为上面这个结论为$\neg q$的论证是无效的，但我找不到下面这个看似能证明它有效的推导过程里的错误：

$$
\begin{align}
(\neg q \land (p \to q)) \to \neg q &\equiv (\neg q \land (\neg p \lor q )) \to \neg q \
&\equiv ((\neg q \land \neg p) \lor (\neg q \land q)) \to \neg q \
&\equiv ((\neg q \land \neg p) \lor \bot) \to \neg q \
&\equiv (\neg q \land \neg p) \to \neg q \
&\equiv \neg(\neg q \land \neg p) \lor \neg q \
&\equiv (q \lor p) \lor \neg q \
&\equiv p \lor (q \lor \neg q) \
&\equiv p \lor \top \
&\equiv \top
\end{align}
$$

其实这里的核心误区是混淆了论证有效性和“推导更有价值的结论”：

• 论证有效性的定义是：如果所有前提为真，结论必然为真。这个论证里，前提本身就包含了$\neg q$，所以只要前提都成立，结论$\neg q$肯定成立，因此这个论证本身是有效的。
• 拒取式得出的$\neg p$是从这两个前提能推导出的另一个有效结论，但这并不代表推导出前提中已有的命题就是无效的。
• 那个推导过程其实是正确的——它只是证明了“前提集合蕴含结论$\neg q$”是一个重言式，这完全符合有效论证的定义，并没有错误。

内容的提问来源于stack exchange，提问作者Cookie