 Intuitionistic (Heyting) arithmetic \(\mathbf{HA}\) and classical (Peano) arithmetic \(\mathbf{PA}\) share the same first-order language and the same non-logical axioms; only the logic is different. In addition to the logical connectives, quantifiers and parentheses and the individual variables \(x, y, z,\ldots\) (also used as metavariables), the language \(L(\mathbf{HA})\) of arithmetic has a binary predicate symbol \(=,\) individual constant \(0,\) unary function constant \(S,\) and finitely or countably infinitely many additional constants for primitive recursive functions including addition and multiplication; the precise choice is a matter of taste and convenience. Terms are built from variables and \(0\) using the function constants; in particular, each natural number \(n\) is expressed in the language by the numeral \(\mathbf{n}\) obtained by applying \(S\) \(n\) times to \(0\) (e.g., \(S(S(0))\) is the numeral for \(2\)). Prime formulas are of the form \((s = t)\) where \(s, t\) are terms, and compound formulas are obtained from these as usual. 