 It was only with the work of Gerhard Gentzen in the early 1930s (see Gentzen 1934, 1935) that researchers in foundations were equipped with formal calculi of deduction that could do real justice to the actual structure of inferential dependencies within mathematical proofs. What we have in mind here are the dependencies of conclusions upon both premises and assumptions that may have been made only “for the sake of argument”. A good example of assumptions of the latter kind are reductio assumptions (assume φ; derive absurdity; conclude ¬φ, now independently of φ). 