Existential instantiation and normalization in sequent natural deduction (Q1198828): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On sequence-conclusion natural deduction systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3743300 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5610986 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3773876 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3994895 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5813181 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5528627 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5582304 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5675348 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Heyting predicate calculus with epsilon symbol / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Remarks on descriptions and natural deduction / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5559220 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5632554 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 16:04, 16 May 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Existential instantiation and normalization in sequent natural deduction |
scientific article |
Statements
Existential instantiation and normalization in sequent natural deduction (English)
0 references
16 January 1993
0 references
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\)''].
0 references
sequent calculus
0 references
variants of natural deduction
0 references
negation rule
0 references
\(\lor\)-elimination
0 references
\(\exists\)-elimination
0 references
\(\varepsilon\)-terms
0 references
normalization
0 references
subformula property
0 references
mid-sequent theorem
0 references
Herbrand theorems
0 references