On Inversion Principles

Abstract

The idea of an ‘inversion principle’, and the name itself, originated in the work of Paul Lorenzen in the 1950s, as a method to generate new admissible rules within a certain syntactic context. Some fifteen years later, the idea was taken up by Dag Prawitz to devise a strategy of normalization for natural deduction calculi (this being an analogue of Gentzen's cut-elimination theorem for sequent calculi). Later, Prawitz used the inversion principle again, attributing it with a semantic role. Still working in natural deduction calculi, he formulated a general type of schematic introduction rules to be matched – thanks to the idea supporting the inversion principle – by a corresponding general schematic Elimination rule. This was an attempt to provide a solution to the problem suggested by the often quoted note of Gentzen. According to Gentzen ‘it should be possible to display the elimination rules as unique functions of the corresponding introduction rules on the basis of certain requirements’. Many people have since worked on this topic, which can be appropriately seen as the birthplace of what are now referred to as “general elimination rules”, recently studied thoroughly by Sara Negri and Jan von Plato. In this study, we retrace the main threads of this chapter of proof-theoretical investigation, using Lorenzen's original framework as a general guide.

Notes

As is well known, in Lorenzen's formulation some formal inaccuracies appear, mainly concerning the role of variables. They are discussed and corrected by H. Hermes in his 1959.

To this same subject, even though focussing on features largely different from that highlighted here, P. Schroeder-Heister has recently devoted various very interesting papers. See for instance Schroeder-Heister 1984 , 2007, in press.

DG[A] for short, when there is no risk of ambiguity.

English translation from the original German in Szabo 1969.

Clearly we assume that the required ‘method’ is meant to be read in terms of the ‘admissibility’ rather than the ‘derivability’ of the elimination rule, but this seems quite a sensible supposition.

We would like to stress that our remarks pertain only to the role attributed to the principle by Negri and von Plato, with respect to the general elimination rules. They do not relate to the proof-theoretical investigations which constitute the core of Negri and von Plato's work and also the topic of Tesconi 2006.