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}$
Might be helpful
No, you cant introduce negation directly like that.
However
$\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$.