Can I use negations in the rules of inference?

Question

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$?

Answer 1

No, modus ponens is not a conjunction. A conjunction consists of a single proposition. Modus ponens has two premises. Also, modus ponens works for implicational propositional calculi where no conjunctions exist.

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.