# Can I use negations in the rules of inference?

For example, modus ponens is $p \land (p → q) \therefore q$.

If I had $¬p$ and $¬q$, could I do $¬p \land (¬p → ¬q) \therefore ¬q$?

• Yes, just as if you could do with any wff substituted for $p,q$, maybe even $(a^2+b^2=c^2)\land (a^2+b^2=c^2\to \gamma=90^\circ)\therefore \gamma=90^\circ$ Commented Jun 27, 2016 at 17:50
• sure ... relabel, $y = ¬p,\ z = ¬q$, and the statement holds for $y,\ z$... just do the substitution Commented Jun 27, 2016 at 17:51
• @HagenvonEitzen: Your comment should be an answer. =) Commented Jun 28, 2016 at 11:21
• @HagenvonEitzen No, modus ponens does not have a conjunction in the antecedent. It has two premises, not one. Commented Jun 29, 2016 at 15:04

You can substitute a negated formula into an inference rule and obtain a derivable rule of inference provided that you substitute the negated formula uniformly for the formula you substitute for. In other words, if you substitute $\alpha$ with $\lnot$p, then wherever $\alpha$ appears in the formula you have to substitute it with $\lnot$p. Your example would then consist of something like {$\lnot$p, ($\lnot$p $\rightarrow$ $\lnot$q)} $\vdash$ $\lnot$q, where $\lnot$p and ($\lnot$p $\rightarrow$ $\lnot$q) consist of distinct premises.