 The proof is given in section II of Ackermann’s paper entitled, tellingly, The consistency proof before the addition of the transfinite axioms. Ackermann uses a logical calculus in axiomatic form that is taken over from Hilbert’s lectures and is discussed below in  section 2.  Here we just note that it involves two logical rules, namely, modus ponens and substitution (for individual, function and statement variables) in axioms. The non-logical axioms concern identity, zero and successor, and recursion equations that define primitive recursive functions. The first step in the argument turns the linear proof into a tree, so that any formula occurrence is used at most once as a premise of an inference (Auflösung in Beweisfäden); this is done in preparation for the second step, namely, the elimination of all necessarily free variables (Ausschaltung der Variablen); in the third step, the numerical value of the closed terms is computed (Reduktion der Funktionale). The resulting syntactic configurations, a Beweisfigur, contains now only numerical formulae that are built up from equations or inequations between numerals and Boolean connectives; these formulae can be effectively determined to be true or false. By induction on the “Beweisfigur” one shows that all its component formulae are true; thus, a formula like \(0\ne 0\) is not provable. The induction principle can be directly incorporated into these considerations when it is formulated as a rule for quantifier-free statements. That was not done in Ackermann’s discussion of the proof, but had been achieved already by Hilbert and Bernays in their 1922/23 lectures.