Contentual and Formal Aspects of Gentzen’s Consistency Proofs

Gentzen’s 1936 consistency proof for first-order arithmetic (Gentzen, Math Ann, 112:493–565, 1936), located between the first (Gentzen, Archiv für mathematische Logik und Grundlagenforschung, 16:97–118, 1974) and third proofs (Gentzen, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, 4:19–44, 1938), was a work during his “transition period 1936–1938.” (Hereafter, we call the first proof the 1935 proof, the second the 1936 proof and the third the 1938 proof.) On the one hand, the 1936 proof inherited from the 1935 proof the method of “finitist (finit)” interpretation for first-order arithmetical formulas.