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?

  • 3
    $\begingroup$ 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$. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '17 at 15:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.