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.


$\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$.

  • $\begingroup$ 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? $\endgroup$ – MonkeyKing Oct 23 '15 at 6:17
  • $\begingroup$ @MonkeyKing that rule follows from introduction of $\land$ and de Morgan's law. $\endgroup$ – mrp Oct 23 '15 at 7:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.