# intermediate calculus between Natural and Sequent Calculus

So as to formalize arithmetic, Gentzen uses an intermediate calculus between the two basic calculi NK and LK. In such calculus, for example, one can deduce $\supset$-elimination rule: $\Delta,\Gamma \Rightarrow 𝔅$ from $\Delta \Rightarrow 𝔄 \supset 𝔅$ and $\Gamma \Rightarrow 𝔄$. My question is how can we obtain the intermediate calculus from Natural deduction NK and Sequent Calculus LK?

• It is simply Natural Deduction written is "sequent-style". For example, $\lor$-elim is: from $\Gamma \to A \lor B$ and $A, \Delta \to C$ and $B, \Theta \to C$, follows: $\Gamma, \Delta, \Theta \to C$. – Mauro ALLEGRANZA Apr 23 '17 at 15:24