 Gödel’s so-called Dialectica intepretation (Gödel 1958) delivers a relative consistency proof and justification for Heyting arithmetic by means of a concrete interpretation involving a system T of computable functionals of finite type. Taken together with his 1933e, which reduces classical first order arithmetic to Heyting arithmetic, a justification in these terms is also obtained for classical first order arithmetic.