[agalunar]

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.

[loicd]

> 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.

Exactly. There is also the matter of efficiency: it is easier to know why something must be true than to know how it's true. Constructibility in mathematics usually means proving things the hard way.