Existential instantiation and normalization in sequent natural deduction (Q1198828)

Gentzen's system of natural deduction, \(\mathbf{NK}\) is not as smooth as his sequent system \({\mathbf{LK}}\) with regard to the negation rule, \(\lor\)-elimination, and \(\exists\)-elimination. The author presents variants of \({\mathbf{NK}}\) that ameliorate these points. As the basic unit of his deduction systems, he takes (not a formula, but) a sequent (i.e. a finite sequence of formulas whose meaning is the disjunction of the component formulas). This resolves the first two difficulties, as in \({\mathbf{LK}}\). To work out the last, the author uses \(\varepsilon\)-terms in a restricted way: in forming a quantified formula, say \(\exists x\varphi(x)\), \(x\) is forbidden to occur in any \(\varepsilon\)-term in \(\varphi(x)\). There are two rules of \(\exists\)-elimination. The first, \((\exists E)\), is the familiar one, namely, from the sequent \(\Delta\), \(\exists x\varphi(x)\) and the deduction of \(\Delta\) from \(\varphi(a)\) with the eigen-variable condition on \(a\), infer \(\Delta\) and discharge \(\varphi(a)\). The second rule, \((\exists E_ \varepsilon)\), states: from \(\Delta\), \(\exists x\varphi(x)\), infer \(\Delta\), \(\varphi(\varepsilon)\), where \(\varepsilon\) is the \(\varepsilon\)-term corresponding to \(\exists x\varphi(x)\). These two rules are shown to be inter-deducible under appropriate conditions. (One direction amounts to a simple case of the second \(\varepsilon\) theorem.) The author proves, mainly for the system with \((\exists E_ \varepsilon)\) but without \((\exists E)\), a number of familiar standard results: the normalization theorem, the subformula property, the mid- sequent theorem, and the Herbrand theorems (the one for existential formulas, and the other for prenex formulas using function symbols). Definitions, theorems, and proofs are all worked out, and a number of examples are exhibited with details. (Hence the length of the paper.) There are some misprints, including a displayed statement of rule. [On p. 116, in \((\neg E)\), ``\(\Lambda,\neg\psi\)'' should be ``\(\Lambda,\neg\varphi\)''].