 They are formulated in the first-order language that has the relation symbols =, &lt;, the function symbols S, +, \(\times\), E and the constant symbol 0. The axioms comprise the usual equations for zero, successor, addition, multiplication, exponentiation, and the less-than relation. In addition, the induction principle is given by the schema   \[\tag{IND} {F(0)} \land {\forall x[F(x)\to F(Sx)]\to \forall x F(x)} \]   for all formulae \(F(x)\) of the language. These principles together with classical logic constitute the theory of first order arithmetic or first order number theory, also known as Dedekind-Peano arithmetic, PA; together with intuitionist logic they constitute intuitionistic first order arithmetic commonly known as Heyting-arithmetic, HA.