It's interesting that although you can't prove "forall P, P or not P" in intuitionistic logic, you can prove "forall P, not (not (P or not P))". In other words, it can't possibly be the case that P is not either true or false.

This is particularly easy to do in Coq:

  Theorem lem : forall (p : Prop), ~ ~ (p \/ ~p).
  Proof.
    tauto.
  Qed.

I personally like the distinction between "this is true" and "this can't possibly be false". If you have a proof of the second, you know why something must be true; if you have a proof of the first, you know how something is true.

The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.