 in Gentzen’s \(\mathcal{N}\) calculus. (As an aid in following this proof, it should be mentioned that Gentzen’s main rule for indirect proofs first generated \(\bot\) (“the absurd proposition”) from the two parts of a contradiction, and then generated the negation of the relevant  assumption.[5]