 The name DNE stands for “double-negation elimination”. There is some controversy over this inference. It is rejected by philosophers and mathematicians who do not hold that each meaningful sentence is either true or not true. Intuitionistic logic does not sanction the inference in question (see, for example Dummett [2000], or the entry on  intuitionistic logic,  or  history of intuitionistic logic),  but, again, classical logic does.