Existential instantiation and normalization in sequent natural deduction
type: Item
instance of: scholarly article
title: Existential instantiation and normalization in sequent natural deduction
zbMATH Open document ID: 0766.03032
DOI: 10.1016/0168-0072(92)90002-H
author: Carlo Cellucci
published in: Annals of Pure and Applied Logic
publication date: 1993-01-16T00:00:00Z
review text: 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 \(…
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B10
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 92989
zbMATH Keywords: sequent calculus
zbMATH Keywords: variants of natural deduction
zbMATH Keywords: negation rule
zbMATH Keywords: \(\lor\)-elimination
zbMATH Keywords: \(\exists\)-elimination
zbMATH Keywords: \(\varepsilon\)-terms
zbMATH Keywords: normalization
zbMATH Keywords: subformula property
zbMATH Keywords: mid-sequent theorem
zbMATH Keywords: Herbrand theorems
MaRDI profile type: Publication
cites work: On sequence-conclusion natural deduction systems
cites work: Q3743300
cites work: Q5610986
cites work: Q3773876
cites work: Q3994895
cites work: Q5813181
cites work: Q5528627
cites work: Q5582304
cites work: Q5675348
cites work: Heyting predicate calculus with epsilon symbol
cites work: Remarks on descriptions and natural deduction
cites work: Q5559220
cites work: Q5632554
description: scientific article; zbMATH DE number 92989