How does $\neg$ distribute over an implication? 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?
 A: $\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?
A: 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)$.
A: 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.
A: It's not distribution, but another useful interaction is that $S \to T$ is equivalent to $(\neg T) \to (\neg S)$.
