 Heyting Arithmetic HA as formulated by Arend Heyting is a formalization of the intuitionistic theory of the natural numbers (Heyting 1956). It has the same non-logical axioms as Peano Arithmetic PA but it is based on intuitionistic logic. Thus it is a restriction of classical arithmetic, and it is the accepted theory of the natural numbers in almost all areas of constructive mathematics. Heyting Arithmetic has many properties that reflect its constructive character, for example the Disjunction Property that holds for intuitionistic logic too. Another property of HA that PA does not share is the numerical existence property: (\(\overline{n}\) is the numeral corresponding to natural number \(n\)) 