How does $\neg$ distribute over an implication?

Question

For example:

$$\neg (\neg (P \to \neg Q) \to \neg R)$$

I'm not sure how the negation on the outside would distribute. Or would it not?

Answer 1

$\neg$ and $\rightarrow$ don't interact in a simple way. Rather, it's best to convert to $\vee$ and $\wedge$ ("or" and "and", in case you've seen other notation), and work there.

For instance, consider "$\neg (P\rightarrow Q)$". Well, "$P\rightarrow Q$" is shorthand for "$Q\vee\neg P$", so we use the rules for negating a disjunction: $$\neg(P\rightarrow Q)=\neg(Q\vee\neg P)=(\neg Q)\wedge (\neg\neg P)=\neg Q\wedge P$$ (which makes sense: "$P\rightarrow Q$" is false if $P$ is true but $Q$ is false).

In this case, you have a more complicated situation, but the same idea works. Your sentence is equivalent to $$\neg[\neg\neg(\neg Q\vee\neg P)\vee \neg R];$$ do you see why, and how to simplify that?

Answer 2

Negation does distribute over implication, but in a way you may at first find surprising: $$\neg\, (p \to q) \equiv (p \land \neg\, q).$$ This follows from De Morgan's law(s), and the fact that $(p \to q) \equiv (\neg\, p \lor q)$.

Answer 3

I like BrianO's answer, but there is another way of looking at it that makes things perhaps more clear (and parts of it work constructively).

First, show that $\lnot p \equiv p \to \bot$, where $\bot$ represents falsity. In constructive logics, this is often the definition of $\lnot p$. Let's do a slight variant where we "undistribute" (sort of) $\lnot$: $$p\to\lnot q \equiv p\to(q \to \bot) \equiv (p\land q)\to\bot\equiv\lnot(p\land q)$$ From a propositions-as-types perspective, this is just uncurrying. We get BrianO's version by choosing $q$ as $\lnot q$ and negating the whole thing, then doing some (non-constructive) double negation eliminations.

Answer 4

It's not distribution, but another useful interaction is that $S \to T$ is equivalent to $(\neg T) \to (\neg S)$.