This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

Provability, Computability and Reflection.

Classical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing calculi can be avoided by borrowing them from (...) MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses. (shrink)

This book argues that the meaning of negation, perhaps the most important logical constant, cannot be defined within the framework of the most comprehensive theory of proof-theoretic semantics, as formulated in the influential work of Michael Dummett and Dag Prawitz. Nils Kürbis examines three approaches that have attempted to solve the problem - defining negation in terms of metaphysical incompatibility; treating negation as an undefinable primitive; and defining negation in terms of a speech act of denial - and concludes that (...) they cannot adequately do so. He argues that whereas proof-theoretic semantics usually only appeals to a notion of truth, it also needs to appeal to a notion of falsity, and proposes a system of natural deduction in which both are incorporated. Offering new perspectives on negation, denial and falsity, his book will be important for readers working on logic, metaphysics and the philosophy of language. (shrink)

Graham Priest takes the relation of identity to be non-transitive. In this paper, we are going to discuss several consequences of identity as a non-transitive relation. We will consider the Henkin-style completeness proof for classical first-order logic with a non-transitive “identity” predicate, Leibniz-identity in Priest’s second-order minimal logic of paradox, and the question whether or not identity of individuals should be defined as Leibniz-identity.

The present monograph is a slightly revised version of my Habilitations schrift Proof-theoretic Aspects of Intensional and Non-Classical Logics, successfully defended at Leipzig University, November 1997. It collects work on proof systems for modal and constructive logics I have done over the last few years. The main concern is display logic, a certain refinement of Gentzen's sequent calculus developed by Nuel D. Belnap. This book is far from offering a comprehensive presentation of generalized sequent systems for modal logics broadly conceived. (...) The proof-theory of non-classical logics is a rapidly developing field, and even the generalizations of the ordinary notion of sequent listed in Chapter 1 can hardly be presented in great detail within a single volume. In addition to further investigating the various approaches toward generalized Gentzen systems, it is important to compare them and to discuss their relative advantages and disadvantages. An initial attempt at bringing together work on different kinds of proof systems for modal logics has been made in [188]. Another step in the same direction is [196]. Since Chapter 1 contains introductory considerations and, moreover, every remaining chapter begins with some surveying or summarizing remarks, in this preface I shall only emphasize a relation to philosophy that is important to me, register the sources of papers that have entered this book in some form or another, and acknowledge advice and support. (shrink)

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by researchers (...) in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations. (shrink)

Model theory is the branch of mathematical logic looking at the relationship between mathematical structures and logic languages. These formal languages are free from the ambiguities of natural languages, and are becoming increasingly important in areas such as computing, philosophy and linguistics. This book provides a clear introduction to the subject for both mathematicians and the non-specialists now needing to learn some model theory.

Identity, we're told, is the binary relation that every object bears to itself, and to itself only. But how can a relation be binary if it never relates two objects? This puzzled Russell and led Wittgenstein to declare that identity is not a relation between objects. The now standard view is that Wittgenstein's position is untenable, and that worries regarding the relational status of identity are the result of confusion. I argue that the rejection of identity as a binary relation (...) is perfectly tenable. To this end, I outline and defend a logical framework that is not committed to an objectual identity relation but is nevertheless expressively equivalent to first-order logic with identity. After it has thus been shown that there is no indispensability argument for objectual identity, I argue that we have good reasons for doubting the existence of such a relation, and rebut a number of attempts at discrediting these reasons. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

We introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, (...) and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

This is a thorough treatment of first-order modal logic. The book covers such issues as quantification, equality (including a treatment of Frege's morning star/evening star puzzle), the notion of existence, non-rigid constants and function symbols, predicate abstraction, the distinction between nonexistence and nondesignation, and definite descriptions, borrowing from both Fregean and Russellian paradigms.

This article is an extended promenade strolling along the winding roads of identity, equality, nameability and completeness, looking for places where they converge. We have distinguished between identity and equality; the first is a binary relation between objects while the second is a symbolic relation between terms. Owing to the central role the notion of identity plays in logic, you can be interested either in how to define it using other logical concepts or in the opposite scheme. In the first (...) case, one investigates what kind of logic is required. In the second case, one is interested in the definition of the other logical concepts in terms of the identity relation, using also abstraction. The present paper investigates whether identity can be introduced by definition arriving to the conclusion that only in full higher-order logic a reliable definition of identity is possible. However, the definition needs the standard semantics and we know that with this semantics completeness is lost. We have also studied the relationship of equality with comprehension and extensionality and pointed out the relevant role played by these two axioms in Henkin’s completeness method. We finish our paper with a section devoted to general semantics, where the role played by the nameable hierarchy of types is the key in Henkin’s completeness method. (shrink)

Natural deduction systems with indefinite and definite descriptions (ε-terms and ι-terms) are presented, and interpreted in Martin-Löf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of 'the element such that the property holds' and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting descriptions by (...) contextual definitions. (shrink)

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.

In the paper we present a relatively simple proof of cut elimination theorem for variety of hybrid logics in the language with satisfaction operators and universal modality. The proof is based on the strategy introduced originally in the framework of hypersequent calculi but it works well also for standard sequent calculi. Sequent calculus examined in the paper works on so called satisfaction formulae and cover all logics adequate with respect to classes of frames defined by so called geometric conditions.

The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account of the notion of (...) meaning is considered. (shrink)

The purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...) of level 2, which when applied to Thinning on the right of level 1 produces intuitionistic out of classical logic (without changing anything else), produces S4 out of S5 (without changing anything else). This characterization of modal constants with sequents of level 2 is unique in the following sense. If constants which differ only graphically are given a formally identical characterization, they can be shown inter-replaceable (not only uniformly) with the original constants salva provability. Customary characterizations of modal constants with sequents of level 1, as well as characterizations in Hilbert-style axiomatizations, are not unique in this sense. This parallels the case with implication, which is not uniquely characterized in Hilbert-style axiomatizations, but can be uniquely characterized with sequents of level 1. These results bear upon theories of philosophical logic which attempt to characterize logical constants syntactically. They also provide an illustration of how alternative logics differ only in their structural rules, whereas their rules for logical constants are identical. (shrink)

Many systems of quantified modal logic cannot be characterised by Kripke's well-known possible worlds semantic analysis. This book shows how they can be characterised by a more general 'admissible semantics', using models in which there is a restriction on which sets of worlds count as propositions. This requires a new interpretation of quantifiers that takes into account the admissibility of propositions. The author sheds new light on the celebrated Barcan Formula, whose role becomes that of legitimising the Kripkean interpretation of (...) quantification. The theory is worked out for systems with quantifiers ranging over actual objects, and over all possibilia, and for logics with existence and identity predicates and definite descriptions. The final chapter develops a new admissible 'cover semantics' for propositional and quantified relevant logic, adapting ideas from the Kripke-Joyal semantics for intuitionistic logic in topos theory. This book is for mathematical or philosophical logicians, computer scientists and linguists. (shrink)

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)

Natural deduction systems with indefinite and definite descriptions are presented, and interpreted in Martin-Löf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of ‘the element such that the property holds' and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting descriptions by contextual definitions.

The paper presents an account of the concept of existence that is based on Brentano’s work. In contrast to Frege and Russell, Brentano took ‘exists’ to express a that subsumes objects and explained it with recourse to the non-propositional attitude of acknowledgment. I argue that the core of Brentano’s view can be developed to a defensible alternative to the Frege-Russell view of existence.