# Rules of natural deduction

In class my professor introduced rules involving

Introduction of $\lor$: $\begin{array}{c} \varphi\\ \hline\hline \varphi \lor \psi \end{array}$

Elimination of $\lor$: $\begin{array}{c} \varphi \lor \psi \quad \varphi\rightarrow a \quad \psi \rightarrow a\\ \hline\hline a \end{array}$

I just wonder can I simply put $\neg$ in? Like rewriting in "negate version"

$\begin{array}{c} \neg \varphi\\ \hline\hline \neg (\varphi \lor \psi) \end{array}$

$\begin{array}{c} \neg (\varphi \lor \psi) \quad \varphi\rightarrow \neg a \quad \psi \rightarrow \neg a\\ \hline\hline a \end{array}$

They seem to be right, but I can't find the proof trees.

Edit: introduction and elimination of $\neg$ were introduced in class:

Introduction: $\begin{array}{c} \varphi\rightarrow \psi \quad \varphi \rightarrow \neg \psi\\ \hline\hline \neg \varphi \end{array}$

Elimination: $\begin{array}{c} \neg \neg \varphi\\ \hline\hline \varphi \end{array}$

$\begin{array}{c} \neg \varphi\\ \hline\hline (\neg \varphi \lor \psi) \end{array}$
and there is no coresponding direct rule for the second one. To see that $\begin{array}{c} \neg \varphi\\ \hline\hline \neg (\varphi \lor \psi) \end{array}$
is not correct, just notice the case where $\psi$ is $\top$ i.e. the predicate which is allways true. Then $\neg(\varphi\vee \psi)$ is allways false, something which we surely should not be able to conclude from any sentence $\neg \varphi$.
• Oh right, I see the first one with no problem. But is $\begin{array}{c} \neg \varphi \quad \neg \psi\\ \hline\hline \neg( \varphi \lor \psi) \end{array}$ legit? (Seems like another version of $\land$) What about the second one? – MonkeyKing Oct 23 '15 at 6:17
• @MonkeyKing that rule follows from introduction of $\land$ and de Morgan's law. – mrp Oct 23 '15 at 7:08