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.

  • $\begingroup$ What do you mean by "derivation rules"? $\endgroup$ – Tiwa Aina Nov 16 '17 at 15:01
  • $\begingroup$ wow I didnt include that in my post. We are only allowed to use the following rules: Conjunction Introduction/Elimination, Disjunction Introduction/Elimination, Conditional Introduction/Elimination, Bicondintional Introduction/Elimination, and negation introduction and elimination. $\endgroup$ – agentnola Nov 16 '17 at 15:02
  • $\begingroup$ You must split the proof on two sub-proofs: $(A \land B) \to \lnot (\lnot A \lor \lnot B)$ and $\lnot (\lnot A \lor \lnot B) \to (A \land B)$ and after use Biconditional-intro rule. $\endgroup$ – Mauro ALLEGRANZA Nov 16 '17 at 15:19
  • $\begingroup$ @agentnola Thanks for the list of rules, but there are many different proof systems, and even if they use this same list of names, there are still differences between different systems how those rules are actually implemented. That is, rules like 'Negation Elimination' or 'Biconditional introduction' can be defined differently between different proof systems. Also, does your system use explicit subproofs? Is there any way you could upload an image or have a link to a webpage, or provide a book reference, so it's cleas what exactly those rules are? $\endgroup$ – Bram28 Nov 16 '17 at 17:16
  • $\begingroup$ @Bram28 We dont really have a complete list. Yes, we have explicit subproofs. I would upload a page or something with all of our rules, but our class no longer uses our text book... $\endgroup$ – agentnola Nov 16 '17 at 18:56

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


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.

  • $\begingroup$ You first prove $\vdash \neg (\neg A\vee \neg B)\to (A\wedge B)$ and $\vdash (A\wedge B)\to\neg(\neg A\vee\neg B)$. This enables you to then use biconditional introduction ("$\sf\leftrightarrow I$") to obtain $\vdash (A\wedge B)\mathop{\leftrightarrow}\neg(\neg A\vee\neg B)$ . $$\dfrac{{\vdash \phi\to \psi\\\vdash \psi\to \phi}}{\vdash \phi\mathop{\leftrightarrow} \psi}{\small\sf \leftrightarrow I}$$ $\endgroup$ – Graham Kemp Nov 16 '17 at 19:53
  • $\begingroup$ Ah, uh... yeah, sure... $\endgroup$ – Ove Ahlman Nov 17 '17 at 12:00

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

  • $\begingroup$ RAA is probably one of (or maybe both) the Negation Introduction/Elimination rules $\endgroup$ – Bram28 Nov 16 '17 at 17:14

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:

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

  • $\begingroup$ See Bram28's answer. The rule called "negation elimination" in Symbolic Logic by David W. Agler, is known as "indirect proof (IP)" in the Open Logic Projects' proof checker. $\endgroup$ – Graham Kemp Aug 14 at 22:22
  • $\begingroup$ @GrahamKemp I don't think Bram28's answer is correct. Lines 20 and 24 reference incorrectly $\neg E$. That rule derives the absurdity symbol. See my lines 14 and 18. What Bram28 is using is called indirect proof as you mention. That implies double negation elimination which cannot be derived using the permitted inference rules for this question. $\endgroup$ – Frank Hubeny Aug 15 at 13:53
  • $\begingroup$ As pointed out, different texts define the rules differently. The OP's text does not use the absurdity symbol, just contrary statements. What it calls negation elimination is: when assumption of a negative derives contradictory statements, you may discharge the assumption to infer the positive. $\endgroup$ – Graham Kemp Aug 15 at 20:36
  • $\begingroup$ @GrahamKemp The OP was given the problem with a constraint to use only certain rules. That is all. The details of those rules were not specified. My suspicion is that the OP was given the problem to show something that could not be shown with intuitionistic rules. $\endgroup$ – Frank Hubeny Aug 15 at 21:04
  • $\begingroup$ Yes, but just listing the name of the rules is often not sufficient, since different systems use the same names for different rules. There isn't a single standard (and that is annoying). When quizzed on this in the comments, the OP clarified that the book was David W. Agler's Symbolic Logic: Semantics, Syntax, and Proof. $\endgroup$ – Graham Kemp Aug 15 at 22:33

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.