[FOM] Re: generalized ND

[Richard Zach]

> From: Sara Negri <negri at cc.helsinki.fi>
> 
> 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.

It might be interesting to some that the generalized rules are exactly
the rules you'd get if you generated them from the truth tables using
the method described in "Systematic construction of natural deduction
systems for many-valued logics"
<http://www.ucalgary.ca/~rzach/papers/mvnd.html> (with Baaz and
Fermüller) and my undergrad thesis "Proof Theory of Finite-Valued
Logics" <http://www.ucalgary.ca/~rzach/papers/ptmvl.html> (both from
'93).

True, these are for multi-conclusion ND systems--it's done in a general
finite-valued framework--and we didn't prove normalization.  It might be
interesting to see if the strong normalization can be carried out in
this general setting. With what's known by now, this might be a project
for an honours thesis/Diplomarbeit.

Best,
Richard

-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Assistant  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada