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. (shrink)

This paper is a study of the opening section of Gentzen’s first publication of 1932,Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen, a text which shows the relevance of Hertz’s work of the 1920’s for the young Gentzen. In fact, Gentzen borrowed from Hertz the analysis of the notion of consequence, which was given in terms of the rules of thinning (Verdünnung) and cut (Schnitt) on sequents (there called “sentences”(Sätze)). Moreover, following Hertz again, he also judged it necessary to justify (...) the forms of inference of the system by providing a semantics for them, so that it became possible to make precise the informal notion of consequence, and to show that the inference rules adopted are correct and sufficient. (shrink)

The paper is devoted to an examination of the epistemic account of the notion of deductive inference recently provided by D. Prawitz, and based on the notion of ground. This is part of the general scenario constituted by the “Proof-theoretic semantics”, presented since the ’70s of the last century as an alternative to the standard model-theoretic explication of the notion of logical consequence.Our argument pivots on the so-called “Curry–Howard Correspondence”, which exploited the idea of considering proofs as proper mathematical objects (...) in a remarkable way. A sort of rational reconstruction of this idea is outlined, tracing it back to Hilbert and Husserl’s investigations. (shrink)

The focus of this paper is on two attempts Sainati made to renew neo-idealistic themes by means of suggestions drawn from the famous Goedel’s Incompleteness Theorems of 1931. Sainati’s remarks on the relationship between «logo astratto » and «logo concreto» are here pursued by reference to some of Goedel’s unpublished texts.

The theory that ``consistency implies existence'' was put forward by Hilbert on various occasions around the start of the last century, and it was strongly and explicitly emphasized in his correspondence with Frege. Since (Gödel's) completeness theorem, abstractly speaking, forms the basis of this theory, it has become common practice to assume that Hilbert took for granted the semantic completeness of second order logic. In this paper I maintain that this widely held view is untrue to the facts, and that (...) the clue to explain what Hilbert meant by linking together consistency and existence is to be found in the role played by the completeness axiom within both geometrical and arithmetical axiom systems. (shrink)

The aim of this paper is to reconsider several proposals that have been put forward in order to develop a Proof-Theoretical Semantics, from the by now classical neo-verificationist approach provided by D. Prawitz and M. Dummett in the Seventies, to an alternative, more recent approach mainly due to the work of P. Schroeder-Heister and L. Hallnäs, based on clausal definitions. Some other intermediate proposals are very briefly sketched. Particular attention will be given to the role played by the so-called Fundamental (...) Assumption. We claim that whereas, in the neo-verificationist proposal, the condition expressed by that Assumption is necessary to ensure the completeness of the justification procedure ( from the outside , so to speak), within the definitional framework it is a built-in feature of the proposal. The latter approach, therefore, appears as an alternative solution to the problem which prompted the neo-verificationists to introduce the Fundamental Assumption. (shrink)