How can I prove that $ \neg (A \Rightarrow B) \iff A \land \neg B$ on a more formal level?

Question

I want to prove that $\neg(A \Rightarrow B) \iff A \land \neg B$ holds without using a truth table.

"$\Leftarrow$": This one is simple: Suppose $A \land \neg B$. We want to show: $(A \Rightarrow B) \Rightarrow \bot$. For that we suppose $A\Rightarrow B$. Now our goal is $\bot$. Since by our assumption $A$ and $A\Rightarrow B$ are true we get $B$ by using Modus ponens. Since $B$ and $\neg B$ holds we get $\bot$ by using Modus ponens again. $\square$

How does "$\Rightarrow$" work?

Thanks in advance!

Answer 1

Following from my comment: the $\Rightarrow$ direction requires that you invoke a non-constructive rule, such as the law of excluded middle or double-negation elimination.

So assume $\neg (A \Rightarrow B)$. Using the law of excluded middle:

• $A \vee \neg A$ is true. If $\neg A$ is true then $A \Rightarrow B$ is true by ex falso—contradiction! So $\neg A$ is true.
• $B \vee \neg B$ is true. If $B$ is true then $A \Rightarrow B$ is true—contradiction! So $\neg B$ is true. [Edit: LEM is not actually required in this step.]

So $A \wedge \neg B$ is true.

Answer 2

You are given $\neg(A \to B)$ [the use of the double arrow for the object-language conditional is to be strongly deprecated, by the way!] You need separate proofs for the two conjuncts.

Suppose $\neg A$. Suppose too $A$, then $\bot$ then $B$. So drop the second supposition and conclude $A \to B$. Contradiction. Hence $\neg\neg A$ and so $A$.

Suppose $B$. Then $A \to B$ (by vacuous conditional proof) so contradiction again. So conclude $\neg B$.

Answer 3

Equivalently, you can prove $[A \implies B] \iff \neg [A \land \neg B]$, which is often given as The Definition in introductory courses, usually with $\equiv$ instead of $\iff$.

See my formal proof of this alternative (only 19 lines) using a form of natural deduction here. It makes use of direct proof, proof by contradiction, and elimination of double negations.