First-order Heyting arithmetic is embedded by various modal translations in modal extensions of first-order Peano arithmetic which are included in Peano S4. Peano arithmetic is embedded by analogous modal translations in an S5-like extension of Heyting arithmetic. This last system is included in the modal extension of Heyting arithmetic where the necessity operator is equivalent to double negation and where Peano arithmetic can be embedded by a modal translation which amounts to a usual double-negation translation.