In classical logic, this is simply true. In constructive logic, it is equivalent to the law of excluded middle (because $\not \not (P \vee \not P)$ is a constructive theorem), and is not assertable in general.

In dependent type theory

In dependent type theory, the law of double negation states that given a type $A$ and a witness that it is an h-proposition, one could derive that one could get an element of $A$ in the context of a function from the function type from $A$ to the empty type to the empty type: