 As part of his “Urdissertation”, Gentzen had established by the end of 1932 the reduction of classical to intuitionist arithmetic, a result that had also been obtained by Gödel. Gentzen’s investigations led, finally in 1935, to his first consistency proof for arithmetic. In the background was a normal form theorem for intuitionist logic that will be discussed in the next section together with Gentzen’s actual dissertation and the special calculi he introduced there. Now we just formulate the Gentzen-Gödel result “connecting” classical first-order number theory PA with its intuitionist version HA. The non-logical principles of these theories aim at describing \(\fN\), the arguably most important structure in mathematics, namely, Dedekind’s simply infinite system \(\bbN\) together with zero, successor, multiplication, exponentiation and the less-than relation: 