[FOM] generalized ND

[Sara Negri]

Dear FOMers,

Concerning the discussion on natural deduction with general
elimination rules, we would like to point out that Schroeder-Heister
(1984) did use the general rule for &-elimination, but his implication
rule instead was a higher-level rule not expressible in predicate
logic. One of us (JvP) found in 1998 independently the implication
rule mentioned by Tennant. Afterwards, it turned out that others had
used it before, including Tennant in 1992. Roy Dyckhoff seems to have
been the first one, in a little-known publication of 1988.

For us, the importance of natural deduction with the general rules is
that it "takes the mystery out of sequent calculus", for it permits to
interpret the structural rules of sequent calculus in terms of natural
deduction: Applications of the rule of weakening correspond to vacuous
discharges, applications of contraction to multiple discharges, and
the other way around. This interpretation stems from translations
between derivations in the two systems and cannot be achieved if the
standard Gentzen-Prawitz natural deduction rules are used.
The general rules also present some advantages in natural deduction
for linear logic: normal form and the subformula property with no
compromises (say explicit weakening) in the rule system (see Negri in
AML's last issue of 2002).

As to our proof of normalization: Felix Joachimski and Ralph Matthes
found in 1999 a proof of strong normalization for our system of
natural deduction with general elimination rules. This has led to a
lot of subsequent work of theirs on normalization in lambda-calculus,
interpolation theorems, etc, (see their home pages in Munich). Strong
normalization having been proved, a proof of mere normalization can
hardly be described as the most important result of our book as
Tennant would have it. We wanted to include the direct proof because
it gave some extra insight into the structure of normal derivations.

The main novelty of "Structural Proof Theory" is, in our opinion, the
extension of proof analysis from pure logic to axiomatic
theories. Mathematical axioms are converted into rules of proof and
proof analysis proceeds through a root-first proof search. For the
termination of such search, the absence of cuts and contractions is of
crucial importance. Continuing this line of research, we have found
that minimum-size derivations sometimes have a "subterm" property,
analogous to Gentzen's subformula property: all terms in such
derivations are known from the endsequent. This gives decidability of
universal formulas as a consequence. For example, we prove this for
linear order, thus achieving a bound for proof search where the
classical result was just decidability in the traditional sense
(=impossibility of undecidability, with no bound). Lattice theory is
another example: Formulated as a system of rules, transitivity is the
only rule in which terms can "vanish", but it permutes up quite
analogously to Gentzen's cut. Projective and affine geometries are a
third example of the subterm property. Amusingly, it is possible to
prove the independence of the parallel postulate by a two-line failed
proof search.


Sara Negri and Jan von Plato

home pages through: "prooftheory.helsinki.fi"