  After his thesis work on ND and SC for pure logic, Gentzen continued his plan of proving the consistency of arithmetic. The result was ready by December 1934. What this very first proof was, is not known in detail. However, a letter to Bernays from 1938 indicates that the proof that Gentzen wrote down by the summer of 1935 was not this original one, but a second proof (see Menzler-Trott 2001, 79). This second proof was criticized by Bernays and Gödel who discussed it during their Atlantic voyage to Princeton in September 1935. Gentzen's idea in the proof was as follows: first, take the conjunction-negation-universal quantification fragment of natural deduction as the logic used in the formalization of arithmetic. Then write each rule instance so that the premisses and conclusion have the open assumptions listed at left, with an arrow separating the conclusion, so, as sequents. This variant of ND is now called ND in SC style. Consider a sequent Γ → C. If its  conclusion is an atomic formula, it is an equation between numbers.  In the worst case it is false, so then consider the list of  assumptions. If one assumption is a conjunction, replace it by a  conjunct of your choice, if a universal quantification, by an  instance. If it is a negation ¬A, replace the conclusion by A. If at any stage of this “reduction  process” the conclusion of a sequent is a compound formula, you have to consider any conjunct or any instance of universal  quantification as a possible conclusion. In case of negation  ¬A as a conclusion, move A to the assumption  part and replace the conclusion by 0 = 1.  Gentzen shows that by  proceeding in this way under the assumption that the sequent in  question is derivable, either a true equation is found as a  conclusion, or a false equation as an assumption. Thus, there are no  derivable sequents with all assumptions true and the conclusion  false.