enter image description here

Here is my attempt, but I'm really not sure if I've done it right; as I'm just about getting the hang of Natural Deduction technique.

Have I done it correctly? If not, where did I make errors and how should I do it?
Thank you in advance!
Sorry for the bad image quality; I'm bad at taking pictures.

  • 1
    $\begingroup$ I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $\equiv$? $\endgroup$ – Git Gud Feb 26 '15 at 9:14
  • $\begingroup$ @GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you! $\endgroup$ – Haxify Feb 26 '15 at 9:24
  • $\begingroup$ Then you can't give a formal proof of $\neg (p\land q)\equiv \neg p\lor \neg q$ because this is a meta-statement. Note that $\neg (p\land q)\leftrightarrow \neg p\lor \neg q$ and $\neg (p\land q)\equiv \neg p\lor \neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague. $\endgroup$ – Git Gud Feb 26 '15 at 9:36
  • $\begingroup$ @GitGud Because of the soundness of Natural Deduction, to prove $\varphi\equiv\psi$ (i.e. $\varphi\vDash\psi$ and $\psi\vDash\varphi$), we can instead prove $\varphi\vdash\dashv\psi$. $\endgroup$ – LoMaPh Feb 26 '15 at 22:15
  • 1
    $\begingroup$ @LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $\bot \text I$ (there's no way that's a badly written $\neg$) and it should be $\neg \neg p$. Same thing on step 10. $\endgroup$ – Git Gud Feb 26 '15 at 22:52

In the second part lines 2 and 7 are redundant, instead assume line 3.

Edit: As noticed by @GitGud, in the first part, line 6 must be $\neg\neg p \ (\neg I)$. So you need to add another line to get $p$ by $(\neg\neg E)$. Similar correction for line 10.

  • $\begingroup$ Oh, I see it. Thank you! Are other parts all fine? $\endgroup$ – Haxify Feb 26 '15 at 8:51
  • $\begingroup$ They seem legit. $\endgroup$ – LoMaPh Feb 26 '15 at 9:08

Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.

Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.

{1}    1. ¬P ∨ ¬Q              premise
{2}    2. P ∧ Q                assumption for proof by contradiction
{2}    3. P                    2 ∧E
{2}    4. Q                    2 ∧E
{5}    5. ¬P                   assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5}  6. P ∧ ¬P               3,5 ∧I
{7}    7. ¬Q                   assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7}  8. Q ∧ ¬Q               4,7 ∧I
{1,2}  9. (P ∧ ¬P) ∨ (Q ∧ ¬Q)  1,5,6,7,8 Discharge 5,7   i.e. ⊥ 
{1}    10. ¬(P ∧ Q)            2,9 proof by contradiction, discharge 2

Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).

11 Feb: Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!


The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:

enter image description here

The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.

As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.

The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.


protected by Community Feb 1 at 17:08

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).

Would you like to answer one of these unanswered questions instead?

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