This problem was recently posed to me that I prove it.
$\vdash (A \land B ) \iff \neg(\neg A \lor \neg B) $
We are only allowed to use derivation rules. It is obviously just the statement of DeMorgan's law. Somehow we have to use biconditional introduction, but when I assume $A \land B$ I can't arrive at $\neg(\neg A \lor \neg B)$.
Thank you in advance.
We are allowed to use the introduction and elimination of the following operators: $\neg, \land, \lor, \Rightarrow \iff$
No other rules are allowed.
$\endgroup$ 84 Answers
$\begingroup$Well, that's a pretty nasty proof ... especially the first half. I doubt you're going to learn any logical reasoning from it, but hey!
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{}{ \fitch{1. A \land B \quad A}{ \fitch{2. \neg A \lor \neg B \quad A}{ \fitch{3. \neg A \quad \quad A}{ \fitch{4. A \land B \quad A}{ 5. A \quad \land E, 4\\ 6.\neg A \quad R, 3 }\\ 7. \neg(A \land B) \quad \neg I, 4-6}\\ \fitch{8. \neg B \quad \quad A}{ \fitch{9. A \land B \quad A}{ 10. B \quad \land E, 10\\ 11.\neg B \quad R, 8 }\\ 12. \neg(A \land B) \quad \neg I, 4-6 }\\ 13. \neg(A \land B) \quad \lor E, \ 2,3-7,8-12\\ 14. A \land B \quad R,1 }\\ 15. \neg (\neg A \lor \neg B) \quad \neg I, 2-14}\\ \fitch{ 16. \neg (\neg A \lor \neg B) \quad A}{ \fitch{ 17. \neg A \quad A}{ 18. \neg A \lor \neg B \quad \lor I, 17\\ 19. \neg (\neg A \lor \neg B) \quad R, 16 }\\ 20. A \quad \neg E, 17-19\\ \fitch{ 21. \neg B \quad A}{ 22. \neg A \lor \neg B \quad \lor I, 21\\ 23. \neg (\neg A \lor \neg B) \quad R, 16 }\\ 24. B \quad \neg E, 21-23\\ 25. A \land B \quad \land I, 20,24 }\\ 26. (A \land B ) \leftrightarrow \neg (\neg A \lor \neg B) \quad \leftrightarrow I, \ 1-15-16-25 }$
$\endgroup$ $\begingroup$I dont know why anyone would like or need to use biconditional introduction to do this. It seems like a very far workaround. Here is a sketch of what you need to do in order to get you going.
When proving $\neg (\neg A \vee \neg B)$ from $A \wedge B$, assume $\neg A\vee \neg B$ and try to arrive at a contradictions. This should be quite straight forward by using $\vee-$elimination and the fact that $A\wedge B$ is already known.
To show $A\wedge B$ from $\neg (\neg A \vee \neg B)$, first assume $\neg A$ then get a contradiction using $\vee-$elimination thus $A$ has to hold secondly just do the same thing for B and thus we arrive at both $A$ and $B$ as conclusions.
$\endgroup$ 2 $\begingroup$Here's the full proof in a calculus called $C_R$, the precise implementation of the rules may vary for your calculus, though.
In $C_R$ you need biconditation introduction, it's the last step in proving a biconditional statement (after you have proved both directions separately). Also I use Reductio Ad Absurdum for the sake of simplicity of the proof.
$[1] \qquad 1 \quad \neg(\neg A \vee\neg B) \qquad \qquad \qquad \quad $A
$[2] \qquad 2 \quad \neg A \qquad \qquad \qquad \qquad\qquad \quad $A
$[2] \qquad 3 \quad \neg A \vee \neg B \qquad \qquad \quad \qquad \quad \vee I. 2$
$[1]\qquad 4 \quad A \qquad \qquad \qquad \quad \quad\qquad \quad $RAA, 1,3,2
$[5]\qquad 5 \quad \neg B \qquad \qquad \qquad \qquad \qquad \quad $A
$[5] \qquad 6 \quad \neg A \vee \neg B \qquad \qquad \qquad \qquad \vee Int 5$
$[1]\qquad 7 \quad B \qquad \qquad \qquad \qquad \qquad \quad $RAA 1,6,5
$[1]\qquad 8 \quad A \wedge B \qquad \qquad \qquad \qquad \quad \wedge Int 4,7$
$[]\quad \qquad 9 \quad \neg(\neg A \wedge \neg B) \Rightarrow A \wedge B \quad \quad \Rightarrow Int 8,1$
$[10]\qquad 10 \quad A \wedge B\qquad \qquad \qquad \qquad \quad $A
$[11] \qquad 11\quad \neg A \vee \neg B \qquad \qquad \qquad \qquad $A
$[10]\qquad 12 \quad A \qquad \qquad \qquad \qquad \qquad \quad \wedge E 10$
$[10]\qquad 13 \quad B \qquad \qquad \qquad \qquad \qquad \quad \wedge E 10$
$[10,11] \quad 14 \quad \neg B \qquad \qquad \qquad \qquad \qquad \vee E 11,12$
$[10] \qquad 15 \quad \neg (\neg A \vee \neg B) \qquad \qquad \qquad \quad $RAA 13,14,11
$[] \qquad \quad 16 \quad A\wedge B \Rightarrow \neg (\neg A \vee \neg B) \qquad\Rightarrow I 15,11$
$[]\qquad \quad 17 \quad A\wedge B \Leftrightarrow \neg (\neg A \vee \neg B) \qquad \Leftrightarrow I 9,16$
I am not sure but I think the calculus is from the book: $\textit{Allen, Colin, and Michael Hand. Logic primer. Mit Press, 2001}$.
$\endgroup$ 1 $\begingroup$The OP asks for a proof of DeMorgan's laws with the following restriction:
We are allowed to use the introduction and elimination of the following operators: ¬,∧,∨,⇒⟺
No other rules are allowed.
Essentially we are restricted to intuitionistic natural deduction inference rules. However, according to the answers to this question Do De Morgan's laws hold in propositional intuitionistic logic?, not all of the four DeMorgan's laws can be shown using intuitionistic logic.
Here is an attempt at a proof that cannot be finished because I am not allowed to use double negation elimination nor indirect proof which I would have used on lines 15 and 19. All I can derive is $\neg \neg A \land \neg \neg B$ which I derive as a compromise on line 20:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker
$\endgroup$ 7
