 The logical axioms and rules of \(\mathbf{HA}\) are those of first-order intuitionistic predicate logic \(\mathbf{IQC}.\) The nonlogical axioms include the reflexive, symmetric and transitive properties of \(=\):  \[ \forall x (x = x),\]   \[ \forall x \forall y (x = y \rightarrow y = x),\]   \[ \forall x \forall y \forall z ((x = y \oldand y = z) \rightarrow x = z);\]  the axiom characterizing \(0\) as the least natural number: