 Other important alternatives to \(\mathbf{H–IQC}\) and \(\mathbf{N–IQC}\) are the various sequent calculi for intuitionistic propositional and predicate logic. The first such calculus was defined by Gentzen [1934–5], cf. Kleene [1952]. Sequent systems, which prove exactly the same formulas as \(\mathbf{H–IQC}\) and \(\mathbf{N–IQC},\) keep track explicitly of all assumptions and conclusions at each step of a proof, replacing modus ponens (which eliminates an intermediate formula) by a cut rule (which can be shown to be an admissible rule (cf. Section 4.2) for the subsystem remaining when it is omitted).