 Gentzen was led to a rule-based calculus with introduction and elimination rules for every logical connective. The truly distinctive feature of this new type of calculus was for Gentzen, however, making and discharging assumptions. This feature, he remarked, most directly reflects a crucial aspect of mathematical  argumentation.[12]  Here we formulate the distinctive rules that involve contradictions and go beyond minimal logic that has I- and E-rules for all logical connectives. Intuitionist logic is obtained from minimal logic by adding the rule: from \(\perp\) infer any formula A, i.e., ex falso quodlibet. In the case of classical logic, if a proof of \(\perp\) is obtained from the assumption \(\neg A\), then infer A (and cancel the assumption \(\neg A\)). Gentzen discovered a remarkable fact for the intuitionist calculus, having observed that proofs can have peculiar detours of the following form: a formula is obtained by an I-rule and is then the major premise of the corresponding E-rule. For conjunction such a detour is depicted as follows: 