Brains, Persons, and Society *** ABSTRACTS    Cervelli, Persone e Società ***ABSTRACTS

Moriconi

The Inversion Principle

The Inversion Principle (IP, for short) has been playing a fundamental role both in the development of proof theory and in the connections between this branch of logic and meaning theoretical investigations.

            Within this evolving framework, the concept of an IP has been exploited for different aims, and even the same expression “IP” has in the time been attributed different meanings. In this talk we wish to retrace the main threads in this discussion, taking into account the pioneer work of Paul Lorenzen, in the Fifties of the last century, which in our opinion is able to provide a broad framework for succeeding developments. In fact, Lorenzen’IP could be phrased as follows: let R be a system of rules such that a certain formula A can be the conclusion only of  the rules

A¹₁,..., A¹_n1  => A; ...; A^j₁,..., A^j_nj  => A

Then the meta-rule

A => B

holds for every formula B; that is to say, the rule A => B is admissible if such are the rules A¹₁,..., A¹_n1  => B; ...; A^j₁,..., A^j_nj  => B (where a rule is admissible if nothing is gained by its addition to the already given system of rules). In other words, once we have produced a certain formula A, it is quite natural to ask which consequences can be drawn from A, given that A can be produced only by means of a well-determined set R of rules. The answer is: all the consequences (meaning: no less than) we can drawn from the premisses of those rules. So that we are allowed to pass directly from those premisses to the consequences of A without any need to make a detour through A.

            Thus, we can say that Lorenzen’s procedure generates Elimination rules in such a way that they are at the same time justified by a reduction warranting their admissibility. In so doing, he paved the way to subsequent developments, leading from Dag Prawitz’s seminal work on Natural Deduction in the Sixties to Sara Negri’s and Jan von Plato’s investigations in Structural Proof Theory in the new century.