  In 1932–33, Gödel and Gentzen found independently of each  other a translation from classical Peano arithmetic to   intuitionistic Heyting arithmetic.  Specifically, it shows that if a contradiction is provable in the  former, it is provable in the latter. Then the consistency of  intuitionistic arithmetic would guarantee also the consistency of  classical arithmetic. This result was a surprise: as mentioned,  Hilbert had thought that the “transfinite” indirect  existence proofs would be the part of arithmetic that needs to be  secured of contradiction. By Gödel's and Gentzen's result,  already intuitionistic arithmetic contained principles that went  beyond finitary reasoning. A letter Gentzen wrote to Heyting on 25  February 1933 summarizes the situation as follows: