-2

It is a great irony of natural deduction that some of the most seemingly obvious inferences are also some of the trickiest to prove! So far, I haven't been able to prove the following, and I'd greatly appreciate if anyone has some nice elegant proofs for them:

~(P & Q) ⊢ ~P ∨ ~Q

~(P→Q) ⊢ P & ~Q

P ↔ Q ⊢ (P & Q) ∨ (~P & ~Q)

~(P ↔ Q) ⊢ (P & ~Q) ∨ (~P & Q)

I have a feeling that if I could get the first of these, the rest would fall out nicely.

PS — Is there a way of formatting logic here? Over at Mathematics they have nice formatting for logic, but I couldn't get it to work here.

Improve this question
3
  • Just a hint and you need to struggle with several assumptions ahead. To crack the first inference in ND, one way to proceed is proof by contradiction. Then just assume ~P, then arrive at ~P ∨ ~Q via ∨-intro rule, then clearly you can get ⊥-intro to let you arrive at P. And symmetrically to do same again to arrive at Q, then you get (P & Q) which is the last contradiction against left side premise. And finally since you have to invoke double negation in the end (or excluded middle for another possible proof route), it's an invalid DeMorgan law in intuitionistic logic...
    – Double Knot
    Jan 13, 2022 at 20:44
  • Unfortunately, no formatting tool available here. You can move the post to MSE...
    – Mauro ALLEGRANZA
    Jan 14, 2022 at 7:26
  • The proof are quite simple... What have you tried on the first two, for example?
    – Mauro ALLEGRANZA
    Jan 14, 2022 at 7:27

1 Answer 1

Reset to default
0 
~(P & Q) ⊢ ~P ∨ ~Q

To prove a disjunction you must either directly prove one of the disjuncts, or use an indirect proof. The second is required here: you cannot derive either alone, just that it cannot be neither.

Here's the start for a Fitch style natural deduction proof. Try to fill in the gap.

 1|_  ~(P & Q)
 2|   |_  ~(~P ∨ ~Q)
 3|   |   |_ P
 4|   |   |   |_ Q


11|   |   ~P ∨ ~Q          ∨i 10
12|   |   #                ~e 11,2
13|   ~~(~P ∨ ~Q)          ~i 2-12
14|   ~P ∨ ~Q              ~~e 13

You can then use that to construct a Genzen style proof tree, (which is much harder to format on this site... so I'm not gonna try).

Improve this answer

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .