 Logics that do not satisfy the negative ex contradictione rule are paraconsistent in a stricter sense. Double negation elimination and classical contraposition fail to be valid in intuitionistic logic (see the entry on  intuitionistic logic);  if one of them is added to an axiom system of intuitionistic logic, one obtains a proof system for classical logic.