  This is not the place to explain the details of ND and SC (but see the entry on automated reasoning).  Gentzen formulated the latter, denoted LK, so that it gave an intuitionistic calculus, denoted LJ, as a special case, the one in which the conclusion is a list of at most one case. He then proved the analogue of the normalization theorem for the classical calculus, the calculus and the proof carefully formulated so that the result for the intuitionistic calculus was a special case of the one for the classical calculus. In LJ and LK, L stands for “logistic”, a term by which Gentzen refers to the axiomatic calculi of logic of Frege, Russell, and Hilbert and Bernays. In such calculi, each line in a derivation is correct in itself, i.e., a logical truth, whence the term. The letters K and J come from the German words klassisch and intuitionistisch. (The latter should thus be upper case "I", but older German uses upper case "J" for upper case "I".)