 According to Bernays, the reductive result due to Gödel and Gentzen,  Theorem 1.2,  has a dramatic impact on the work concerned with Hilbert’s program. It opened in a very concrete and precise way the finitist perspective to a broader “constructive” one. Hilbert himself had taken such a step in a much vaguer way in his last paper (Hilbert 1931b).  Theorem 1.2  showed, after all, that PA is contained in HA via the negative translation. Since HA comprises just a fragment of Brouwer’s intuitionism, the consistency of PA is secured on the basis of the intuitionist standpoint. In a letter to Heyting of 25 February 1933, Gentzen suggested investigating the consistency of HA since a consistency proof for classical arithmetic had not been given so far by finitist means. He then continued