 He actually worked on a consistency proof for analysis as letters  (e.g. one to Bernays on 23.6.1935 translated in von Plato 2017: 240) and stenographic notes from 1945 (e.g., Gentzen 1945) show. Formally, “analysis” was identified already in Hilbert 1917/18 as a form of second order number theory. Hilbert and Bernays developed mathematical analysis in a supplement of the second volume of their “Grundlagen der Mathematik”. We take \(\bZ_2\) as given in the following way. Its language extends that of PA by an additional sort of variables \(X,Y,Z,\ldots\) that range over sets of numbers and the binary membership relation \(t\in X\). Its axioms are those of PA, but the principle of proof by induction is formulated as the second order induction axiom 