He used the Gödel–Gentzen negative translation to prove in 1933 that if HA is consistent, then PA is also consistent.
Er verwendete die Gödel-Gentzen-Übersetzung, um 1933 zu beweisen, dass wenn HA konsistent ist, so auch PA.