On sequence-conclusion natural deduction systems (Q1062053): Difference between revisions

The sequence-conclusion approach to natural deduction is a generalization of the well-known Gentzen approach. We suppose that the premises and the conclusion of any inference rule are finite sequences of formulae. So, for instance, the rules for the introduction and elimination of the implication will be as follows \[ [A]\frac{\Delta,B}{\Delta,A\to B}\quad and\quad \frac{\Delta,A\quad \Lambda,A\to B}{\Delta,\Lambda,B}. \] In such a case we are able to get a normalizable and separable natural deduction formulation of classical logic. The main result of the paper is the normal form theorem for given formulation of the classical first order logic obtained as a consequence of the cut elimination theorem for the corresponding sequent calculus.