. The term inversion principle goes back to Lorenzen who coined it in the early 1950s. It was later used by Prawitz and others to describe the symmetric relationship between introduction and elimination inferences in natural deduction, sometimes also called harmony. In dealing with the invertibility of rules of an arbitrary atomic production system, Lorenzen’s inversion principle has a much wider range than Prawitz’s adaptation to natural deduction. It is closely related to definitional reflection, which is a principle for reasoning (...) on the basis of rule-based atomic definitions, proposed by Hallnäs and Schroeder-Heister. After presenting definitional reflection and the inversion principle, it is shown that the inversion principle can be formally derived from definitional reflection, when the latter is viewed as a principle to establish admissibility. Furthermore, the relationship between definitional reflection and the inversion principle is investigated on the background of a universalization principle, called the ω- principle, which allows one to pass from the set of all defined substitution instances of a sequent to the sequent itself. (shrink)

The paper studies admissibility of multiple-conclusion rules in positive logics. Using modification of a method employed by M. Wajsberg in the proof of the separation theorem, it is shown that the problem of admissibility of multiple-conclusion rules in the positive logics is equivalent to the problem of admissibility in intermediate logics defined by positive additional axioms. Moreover, a multiple-conclusion rule \ follows from a set of multiple-conclusion rules \ over a positive logic \ if and only if \ follows from (...) \ over \. (shrink)

The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used in normalization theory. It (...) is argued that these two sorts of concepts must be kept strictly apart. (shrink)

There is an ambiguity in the concept of deductive validity that went unnoticed until the middle of the twentieth century. Sometimes an inference rule is called valid because its conclusion is a theorem whenever its premises are. But often something different is meant: The rule's conclusion follows from its premises even in the presence of other assumptions. In many logical environments, these two definitions pick out the same rules. But other environments are context-sensitive, and in these environments the second notion (...) is stronger. Sorting out this ambiguity has led to profound mathematical investigations with applications in complexity theory and computer science. The origins of this ambiguity and the history of its resolution deserve philosophical attention, because our understanding of logic stands to benefit from their details. I am eager to examine together with you, Crito, whether this argument will appear in any way different to me in my present circumstances, or whether it remains the same, whet... (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)