Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of such systems from logic (...) to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

This book introduces an important group of logics that have come to be known under the umbrella term 'susbstructural'. Substructural logics have independently led to significant developments in philosophy, computing and linguistics. _An Introduction to Substrucural Logics_ is the first book to systematically survey the new results and the significant impact that this class of logics has had on a wide range of fields.The following topics are covered: * Proof Theory * Propositional Structures * Frames * Decidability * Coda Both (...) students and professors of philosophy, computing, linguistics, and mathematics will find this to be an important addition to their reading. (shrink)

Logical pluralism is the view that different logics are equally appropriate, or equally correct. Logical relativism is a pluralism according to which validity and logical consequence are relative to something. Stewart Shapiro explores various such views. He argues that the question of meaning shift is itself context-sensitive and interest-relative.

Adding a transparent truth predicate to a language completely governed by classical logic is not possible. The trouble, as is well-known, comes from paradoxes such as the Liar and Curry. Recently, Cobreros, Egré, Ripley and van Rooij have put forward an approach based on a non-transitive notion of consequence which is suitable to deal with semantic paradoxes while having a transparent truth predicate together with classical logic. Nevertheless, there are some interesting issues concerning the set of metainferences validated by this (...) logic. In this paper, we show that this logic, once it is adequately understood, is weaker than classical logic. Moreover, the logic is in a way similar to the paraconsistent logic LP. (shrink)

Logic, Logical connectives, Verbal disputes, Proof theory, Non-classical logic.

This paper presents and motivates a new philosophical and logical approach to truth and semantic paradox. It begins from an inferentialist, and particularly bilateralist, theory of meaning---one which takes meaning to be constituted by assertibility and deniability conditions---and shows how the usual multiple-conclusion sequent calculus for classical logic can be given an inferentialist motivation, leaving classical model theory as of only derivative importance. The paper then uses this theory of meaning to present and motivate a logical system---ST---that conservatively extends classical (...) logic with a fully transparent truth predicate. This system is shown to allow for classical reasoning over the full (truth-involving) vocabulary, but to be non-transitive. Some special cases where transitivity does hold are outlined. ST is also shown to give rise to a familiar sort of model for non-classical logics: Kripke fixed points on the Strong Kleene valuation scheme. Finally, to give a theory of paradoxical sentences, a distinction is drawn between two varieties of assertion and two varieties of denial. On one variety, paradoxical sentences cannot be either asserted or denied; on the other, they must be both asserted and denied. The target theory is compared favourably to more familiar related systems, and some objections are considered. (shrink)

Logical pluralism is the claim that different accounts of validity can be equally correct. Beall and Restall have recently defended this position. Validity is a matter of truth-preservation over cases, they say: the conclusion should be true in every case in which the premises are true. Each logic specifies a class of cases, but differs over which cases should be considered. I show that this account of logic is incoherent. Validity indeed is truth-preservation, provided this is properly understood. Once understood, (...) there is one true logic, relevance logic. The source of Beall and Restall’s error is a recent habit of using a classical metalanguage to analyse non-classical logics generally, including relevance logic. (shrink)

Consequence is at the heart of logic; an account of consequence, of what follows from what, offers a vital tool in the evaluation of arguments. Since philosophy itself proceeds by way of argument and inference, a clear view of what logical consequence amounts to is of central importance to the whole discipline. In this book JC Beall and Greg Restall present and defend what thay call logical pluralism, the view that there is more than one genuine deductive consequence relation, a (...) position which has profound implications for many linguists as well as for philosophers. We should not search for one true logic, since there are many. (shrink)

This highly acclaimed book is a major contribution to the philosophy of language as well as a systematic interpretation of Frege, indisputably the father of ...

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

Dialetheism is the view that some contradictions are true. This is a view which runs against orthodoxy in logic and metaphysics since Aristotle, and has implications for many of the core notions of philosophy. Doubt Truth to Be a Liar explores these implications for truth, rationality, negation, and the nature of logic, and develops further the defense of dialetheism first mounted in Priest's In Contradiction, a second edition of which is also available.

Such a conception, says Dummett, will form "a base camp for an assault on the metaphysical peaks: I have no greater ambition in this book than to set up a base ...

It will be an essential resource for philosophers, mathematicians, computer scientists, linguists, or any scholar who finds connectives, and the conceptual issues surrounding them, to be a source of interest.This landmark work offers both ...

In the 1920s, Paul Hertz (1881-1940) developed certain calculi based on structural rules only and established normal form results for proofs. It is shown that he anticipated important techniques and results of general proof theory as well as of resolution theory, if the latter is regarded as a part of structural proof theory. Furthermore, it is shown that Gentzen, in his first paper of 1933, which heavily draws on Hertz, proves a normal form result which corresponds to the completeness of (...) prepositional SLD-resolution in logic programming. (shrink)

We provide a general investigation of Logic in which the notion of a simple consequence relation is taken to be fundamental. Our notion is more general than the usual one since we give up monotonicity and use multisets rather than sets. We use our notion for characterizing several known logics (including Linear Logic and non-monotonic logics) and for a general, semantics-independent classi cation of standard connectives via equations on consequence relations (these include Girard's \multiplicatives" and \additives"). We next investigate the (...) standard methods for uniformly representing consequence relations: Hilbert type, Natural Deduction and Gentzen type. The advantages and disadvantages of using each system and what should be taken as.. (shrink)

Consequence is at the heart of logic; an account of consequence, of what follows from what, offers a vital tool in the evaluation of arguments. Since philosophy itself proceeds by way of argument and inference, a clear view of what logical consequence amounts to is of central importance to the whole discipline. In this book JC Beall and Greg Restall present and defend what thay call logical pluralism, the view that there is more than one genuine deductive consequence relation, a (...) position which has profound implications for many linguists as well as for philosophers. We should not search for one true logic, since there are many. (shrink)

General-elimination harmony articulates Gentzen’s idea that the elimination-rules are justified if they infer from an assertion no more than can already be inferred from the grounds for making it. Dummett described the rules as not only harmonious but stable if the E-rules allow one to infer no more and no less than the I-rules justify. Pfenning and Davies call the rules locally complete if the E-rules are strong enough to allow one to infer the original judgement. A method is given (...) of generating harmonious general-elimination rules from a collection of I-rules. We show that the general-elimination rules satisfy Pfenning and Davies’ test for local completeness, but question whether that is enough to show that they are stable. Alternative conditions for stability are considered, including equivalence between the introduction- and elimination-meanings of a connective, and recovery of the grounds for assertion, finally generalizing the notion of local completeness to capture Dummett’s notion of stability satisfactorily. We show that the general-elimination rules meet the last of these conditions, and so are indeed not only harmonious but also stable. (shrink)

The logician's central concern is with the validity of argument. A logical theory ought, therefore, to provide a general criterion of validity. This book sets out to find such a criterion, and to describe the philosophical basis and the formal theory of a logic in which the premises of a valid argument are relevant to its conclusion. The notion of relevance required for this theory is obtained by an analysis of the grounds for asserting a formula in a proof.

This paper argues that logical inferentialists should reject multiple-conclusion logics. Logical inferentialism is the position that the meanings of the logical constants are determined by the rules of inference they obey. As such, logical inferentialism requires a proof-theoretic framework within which to operate. However, in order to fulfil its semantic duties, a deductive system has to be suitably connected to our inferential practices. I argue that, contrary to an established tradition, multiple-conclusion systems are ill-suited for this purpose because they fail (...) to provide a 'natural' representation of our ordinary modes of inference. Moreover, the two most plausible attempts at bringing multiple conclusions into line with our ordinary forms of reasoning, the disjunctive reading and the bilateralist denial interpretation, are unacceptable by inferentialist standards. (shrink)

The concept of truth arguably plays a central role in many areas of philosophical theorizing. Yet, what seems to be one of the most fundamental principles governing that concept, i.e. the equivalence between P and , is inconsistent in full classical logic, as shown by the semantic paradoxes. I propose a new solution to those paradoxes, based on a principled revision of classical logic. Technically, the key idea consists in the rejection of the unrestricted validity of the structural principle of (...) contraction. I first motivate philosophically this idea with the metaphysical picture of the states-of-affairs expressed by paradoxical sentences as being distinctively . I then proceed to demonstrate that the theory of truth resulting from this metaphysical picture is, in many philosophically interesting respects, surprisingly stronger than most other theories of truth endorsing the equivalence between P and (for example, the theory vindicates the validity of the traditional laws of excluded middle and of non-contradiction, and also vindicates the traditional constraint of truth preservation on logical consequence). I conclude by proving a cutelimination theorem that shows the consistency of the theory. (shrink)

Logic is essential to correct reasoning and also has important theoretical applications in philosophy, computer science, linguistics, and mathematics. This book provides an exceptionally clear introduction to classical logic, with a unique approach that emphasizes both the hows and whys of logic. Here Nicholas Smith thoroughly covers the formal tools and techniques of logic while also imparting a deeper understanding of their underlying rationales and broader philosophical significance. In addition, this is the only introduction to logic available today that presents (...) all the major forms of proof--trees, natural deduction in all its major variants, axiomatic proofs, and sequent calculus. The book also features numerous exercises, with solutions available on an accompanying website. -/- Logic is the ideal textbook for undergraduates and graduate students seeking a comprehensive and accessible introduction to the subject. -/- Provides an essential introduction to classical logic Emphasizes the how and why of logic Covers both formal and philosophical issues Presents all the major forms of proof--from trees to sequent calculus Features numerous exercises, with solutions available online The ideal textbook for undergraduates and graduate students . (shrink)

In this paper investigates how natural deduction rules define connective meaning by presenting a new method for reading semantical conditions from rules called natural semantics. Natural semantics explains why the natural deduction rules are profoundly intuitionistic. Rules for conjunction, implication, disjunction and equivalence all express intuitionistic rather than classical truth conditions. Furthermore, standard rules for negation violate essential conservation requirements for having a natural semantics. The standard rules simply do not assign a meaning to the negation sign. Intuitionistic negation fares (...) much better. Not only do the intuitionistic rules have a natural semantics, that semantics amounts to familiar intuitionistic truth conditions. We will make use of these results to argue that intuitionistic connectives, rather than standard ones have a better claim to being the truly logical connectives. (shrink)

Our topic is the notion of logical consequence: the link between premises and conclusions, the glue that holds together deductively valid argument. How can we understand this relation between premises and conclusions? It seems that any account begs questions. Painting with very broad brushtrokes, we can sketch the landscape of disagreement like this: “Realists” prefer an analysis of logical consequence in terms of the preservation of truth [29]. “Anti-realists” take this to be unhelpful and o:er alternative analyses. Some, like Dummett, (...) look to preservation of warrant to assert [9, 36]. Others, like Brandom [5], take inference as primitive, and analyse other notions in terms of it. There is plenty of disagreement on the “realist” side of the fence too. It is one thing to argue that logical consequence involves preservation of truth. It is another to explain how far truth must be preserved. Is the preservation essentially modal (in all circumstances [25]) or analytic (vouchsafed by.. (shrink)

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall investigate (...) the relation between Linear Logic and previously known systems, especially Relevance logics. (shrink)

Arguments, the story goes, have one or more premises and only one conclusion. A contentious generalisation allows arguments with several disjunctively connected conclusions. Contentious as this generalisation may be, I will argue nevertheless that it is justified. My main claim is that multiple conclusions are epiphenomena of the logical connectives: some connectives determine, in a certain sense, multiple-conclusion derivations. Therefore, such derivations are completely natural and can safely be used in proof-theoretic semantics.

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. As (...) recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (shrink)

In a famous and controversial paper, B. H. Slater has argued against the possibility of paraconsistent logics. Our reply is centred on the distinction between two aspects of the meaning of a logical constant *c* in a given logic: its operational meaning, given by the operational rules for *c* in a cut-free sequent calculus for the logic at issue, and its global meaning, specified by the sequents containing *c* which can be proved in the same calculus. Subsequently, we use the (...) same strategy to counter Quine's meaning variance argument against deviant logics. In a nutshell, we claim that genuine rivalry between (similar) logics *L* and *L'* is possible whenever each constant in *L* has the same operational meaning as its counterpart in *L'* although differences in global meaning arise in at least one case. (shrink)

The aim of the present book is to give a comprehensive account of the ‘state of the art’ of substructural logics, focusing both on their proof theory and on their semantics (both algebraic and relational. It is for graduate students in either philosophy, mathematics, theoretical computer science or theoretical linguistics as well as specialists and researchers.

Michael Dummett; VIII.—Truth, Proceedings of the Aristotelian Society, Volume 59, Issue 1, 1 June 1959, Pages 141–162, https://doi.org/10.1093/aristotelian/59.1.

The sequent system LDJ is formulated using the same connectives as Gentzen's intuitionistic sequent system LJ, but is dual in the following sense: (i) whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii) whereas LJ has the same sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain a (...) more precise mapping, both LJ and LDJ are extended by adding a "pseudo-difference" operator which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems and , and a simply consistent but -inconsistent Set Theory with Unrestricted Comprehension Schema based on LDJ is sketched. (shrink)

Michael Dummett and Dag Prawitz have argued that a constructivist theory of meaning depends on explicating the meaning of logical constants in terms of the theory of valid inference, imposing a constraint of harmony on acceptable connectives. They argue further that classical logic, in particular, classical negation, breaks these constraints, so that classical negation, if a cogent notion at all, has a meaning going beyond what can be exhibited in its inferential use. I argue that Dummett gives a mistaken elaboration (...) of the notion of harmony, an idea stemming from a remark of Gerhard Gentzen's. The introduction-rules are autonomous if they are taken fully to specify the meaning of the logical constants, and the rules are harmonious if the elimination-rule draws its conclusion from just the grounds stated in the introduction-rule. The key to harmony in classical logic then lies in strengthening the theory of the conditional so that the positive logic contains the full classical theory of the conditional. This is achieved by allowing parametric formulae in the natural deduction proofs, a form of multiple-conclusion logic. (shrink)

Published with the aid of a grant from the National Endowment for the Humanities. Contains the only complete English-language text of The Concept of Truth in Formalized Languages. Tarski made extensive corrections and revisions of the original translations for this edition, along with new historical remarks. It includes a new preface and a new analytical index for use by philosophers and linguists as well as by historians of mathematics and philosophy.

This note motivates a logic for a theory that can express its own notion of logical consequence—a ‘syntactically closed’ theory of naive validity. The main issue for such a logic is Curry’s paradox, which is averted by the failure of contraction. The logic features two related, but different, implication connectives. A Hilbert system is proposed that is complete and non-trivial.

Beall and Restall’s Logical Pluralism (2006) characterises pluralism about logical consequence in terms of the different ways cases can be selected in the analysis of logical consequence as preservation of truth over a class of cases. This is not the only way to understand or to motivate pluralism about logical consequence. Here, I will examine pluralism about logical consequence in terms of different standards of proof. We will focus on sequent derivations for classical logic, imposing two different restrictions on classical (...) derivations to produce derivations for intuitionistic logic and for dual intuitionistic logic. The result is another way to understand the manner in which we can have different consequence relations in the same language. Furthermore, the proof-theoretic perspective gives us a different explanation of how the one concept of negation can have three different truth conditions, those in classical, intuitionistic and dual-intuitionistic models. (shrink)

The philosophical discussion about logical constants has only recently moved into the substructural era. While philosophers have spent a lot of time discussing the meaning of logical constants in the context of classical versus intuitionistic logic, very little has been said about the introduction of substruc-tural connectives. Linear logic, affine logic and other substructural logics offer a more fine-grained perspective on basic connectives such as conjunction and disjunction, a perspective which I believe will also shed light on debates in the (...) philosophy of logic. In what follows I will look at one particularly interesting instance of this: The development of the position known as logical inferentialism in view of substructural connectives. I claim that sensitivity to structural properties is an interesting challenge to logical inferentialism, and that it ultimately requires revision of core notions in the inferentialist litera-ture. Specifically, I want to argue that current definitions of proof theoretic harmony give rise to problematic nonconservativeness as a result of their insensitivity to substructurality. These nonconservativeness results are undesirable because they make it impossible to consistently add logical constants that are of independent philosophical interest. (shrink)