 The Hilbert-style system \(\mathbf{H–IQC}\) is useful for metamathematical investigations of intuitionistic logic, but its forced linearization of deductions and its preference for axioms over rules make it an awkward instrument for establishing derivability. A natural deduction system \(\mathbf{N–IQC}\) for intuitionistic predicate logic results from the deductive system \(\mathbf{D},\) presented in Section 3 of the entry on  classical logic  in this Encyclopedia, by omitting the symbol and rules for identity, and replacing the classical rule (DNE) of double negation elimination by the intuitionistic negation elimination rule expressing ex falso: 