  In pursuing his consistency program, Gentzen set as his first task the analysis of purely logical deduction, to be extended later to arithmetic and analysis. In his thesis (1934–1935), Gentzen states that he set as his task the analysis of mathematical proofs as they occur in practice.  The first observation is that actual proofs are not based on axioms expressed in a logical language, as in Hilbert's axiomatic proof theory. The most typical feature is instead that theorems make their claims under some assumptions. The assumptions are analyzed into parts and the conclusion is also analyzed into parts until these two analyses meet and a proof can be synthesized.  The latter analysis proceeds by what Gentzen called introduction rules: they give sufficient conditions for deriving a proposition of a given form. For example, to derive a conjunction A &amp; B, it is sufficient to derive the conjuncts A and B separately. The inference is given formally as in the rule