 We now consider Gödel 1933e, in which Gödel showed, in effect, that intuitionistic or Heyting arithmetic is only apparently weaker than classical first-order arithmetic. This is because the latter can be interpreted within the former by means of a simple translation, and thus to be convinced of the consistency of classical arithmetic, it is enough to be convinced of the consistency of Heyting arithmetic. Heyting arithmetic is defined to be the same as classical arithmetic, except that the underlying predicate logic is given by intuitionistic axioms and rules of inference (see below).