MHB Natural deduction (negated implication)

[Logic1]

The proposition ¬(P→Q) is equivalent to ¬P^Q

Does someone maybe have an idea how you can prove (directly) ¬P^Q from ¬(P→Q) by means of natural deduction? I do not manage it.

Thanks in advance!

 

[Ackbach]

I would disagree with the problem. It's true that $\lnot(p\to q) \equiv (p\land\lnot q),$ but it is not true that $\lnot(p\to q)\equiv(\lnot p \land q)$. (A quick truth table will tell you this.) So you need to prove $\lnot(p\to q) \implies (p\land\lnot q)$ and you need to prove $(p\land\lnot q) \implies \lnot(p\to q)$.

Let's take the first one: $\lnot(p\to q) \implies (p\land\lnot q)$. What logical symbols $(\lnot, \land, \lor, \to, \equiv)$ are present/absent in the conclusion versus the premise? Well, we see that there's a $\to$ in the premise, but not in the conclusion, and there's a $\land$ in the conclusion that's not in the premise. So we might well need $\to$ elimination, as well as $\land$ introduction. You see how that can help you structure your proof?

 

[Logic1]

Thank Ackbach!

I made a typing error I think. I meant ¬(p→q)⟹(p∧¬q) of course.

To apply the ∧-introduction, I need to get P and ¬Q. But I do not see yet which steps I can start with to make the →-elimination possible (it's clearly not applicable immediately).

 

[Ackbach]

Thank Ackbach!

I made a typing error I think. I meant ¬(p→q)⟹(p∧¬q) of course.

To apply the ∧-introduction, I need to get P and ¬Q. But I do not see yet which steps I can start with to make the →-elimination possible (it's clearly not applicable immediately).

Right, exactly. I would think about using $\lnot$ elimination. It's a powerful method, because you can construct sub-proofs by assuming anything you want. Don't forget contradiction elimination, where you can conclude anything you want from a contradiction. That's an important proof technique in subproofs. What outline do you have?

 

[Ackbach]

Here's what I mean by outline, and this is what I would recommend for you to do. Basically, you're going to use $\land$ intro as the main organizing principle.

View attachment 7751

 

[solakis1]

Here's what I mean by outline, and this is what I would recommend for you to do. Basically, you're going to use $\land$ intro as the main organizing principle.

Is step 2 hypothesis for contradiction??

 

[Ackbach]

Is step 2 hypothesis for contradiction??

Yep, that's right!

 

[solakis1]

Yep, that's right!

Then on the 6th step we should have ~~P and not on the 8th step

 

[Ackbach]

Then on the 6th step we should have ~~P and not on the 8th step

Well, that just depends on how many steps it takes you to get a contradiction. No doubt you are more efficient at it than I am.