This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...) subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

In this note, we review paradoxes like Russell’s, the Liar, and Curry’s in the context of intuitionistic logic. One may observe that one cannot blame the underlying logic for the paradoxes, but has to take into account the particular concept formations. For proof-theoretic semantics, however, this comes with the challenge to block some forms of direct axiomatizations of the Liar. A proper answer to this challenge might be given by Schroeder-Heister’s definitional freedom.

The paper introduces a new type of rules into Natural Deduction, elimination rules by composition. Elimination rules by composition replace usual elimination rules in the style of disjunction elimination and give a more direct treatment of additive disjunction, multiplicative conjunction, existence quantifier and possibility modality. Elimination rules by composition have an enormous impact on proof-structures of deductions: they do not produce segments, deduction trees remain binary branching, there is no vacuous discharge, there is only few need of permutations. This new (...) type of rules fits especially to substructural issues, so it is shown for Lambek Calculus, i.e. intuitionistic non-commutative linear logic and to its extensions by structural rules like permutation, weakening and contraction. Natural deduction formulated with elimination rules by composition from a complexity perspective is superior to other calculi. (shrink)

The article introduces substructural epistemic logics of belief supported by evidence. The logics combine normal modal epistemic logics with distributive substructural logics. Pieces of evidence are represented by points in substructural models and availability of evidence is modelled by a function on the point set. The main technical result is a general completeness theorem. Axiomatisations are provided by means of two-sorted Hilbert-style calculi. It is also shown that the framework presents a natural solution to the problem of logical omniscience.

It is proved that MacLane's coherence results for monoidal and symmetric monoidal categories can be extended to some other categories with multiplication; namely, to relevant, affine and cartesian categories. All results are formulated in terms of natural transformations equipped with “graphs” (g-natural transformations) and corresponding morphism theorems are given as consequences. Using these results, some basic relations between the free categories of these classes are obtained.

This book sets out the foundations, methodology, and practice of a formal framework for the description of language. The approach embraces the trends of lexicalism and compositional semantics in computational linguistics, and theoretical linguistics more broadly, by developing categorial grammar into a powerful and extendable logic of signs. Taking Montague Grammar as its point of departure, the book explains how integration of methods from philosophy (logical semantics), computer science (type theory), linguistics (categorial grammar) and meta-mathematics (mathematical logic ) provides a (...) categorial foundation with coverage including intensionality, quantification, featural polymorphism, domains and constraints. For the first time, the book systematises categorial thinking into a unified program which is at once both logically secured, and a practical tool for pure lexical grammar development with type-theoretic semantics. It should be of interest to all those active in computational linguistics and formal grammar and is suitable for use at advanced undergraduate, postgraduate, and research levels. (shrink)

This article begins by exploring a lost topic in the philosophy of science:the properties of the relations evidence confirming h confirmsh'' and, more generally, evidence confirming each ofh1, h2, ..., hm confirms at least one of h1, h2,ldots;, hn''.The Bayesian understanding of confirmation as positive evidential relevanceis employed throughout. The resulting formal system is, to say the least, oddlybehaved. Some aspects of this odd behaviour the system has in common withsome of the non-classical logics developed in the twentieth century. Oneaspect (...) – its ``parasitism'''' on classical logic – it does not, and it is this featurethat makes the system an interesting focus for discussion of questions in thephilosophy of logic. We gain some purchase on an answer to a recently prominentquestion, namely, what is a logical system? More exactly, we ask whether satisfaction of formal constraints is sufficient for a relation to be considered a (logical) consequence relation. The question whether confirmation transfer yields a logical system is answered in the negative, despite confirmation transfer having the standard properties of a consequence relation, on the grounds that validity of sequents in the system is not determined by the meanings of the connectives that occur in formulas. Developing the system in a different direction, we find it bears on the project of ``proof-theoretic semantics'''': conferring meaning on connectives by means of introduction (and possibly elimination) rules is not an autonomous activity, rather it presupposes a prior, non-formal,notion of consequence. Some historical ramifications are alsoaddressed briefly. (shrink)

RésuméUn paradigme en vogue en informatique théorique exploite l'analogie entre les formules et les types et traite une deduction Al… An→ B comme une opération plurisortale. On propose ici d'étendre cette analogie aux déductions de la forme Al… An→, où la place à droite de la flèche est vide. D'un point de vue logique, une telle déduction constitue une réfutation de la conjonction desformules qui se trouvent à gauche de la flèche. On défend l'idée qu'ilfaut, selon ce paradigme étendu, interpréter (...) la flèche comme assignant à n'importe quelle séquence al… an, où aiest de type Ai, le type des valeurs de vérite correspondantes. Pour que cela fonctionne, cependant, il faut abandonner la règle structurale de l'affaiblissement à droite de la flèche. La négation de A est alors interprétée comme l'ensemble puissance de A et la complétude fonctionnelle habituelle s'identifie au schème de compréhension avec extensionnalitè. (shrink)

We prove a representation theorem for residuated algebras: each residuated algebra is isomorphically embeddable into a powerset residuated algebra. As a consequence, we obtain a completeness theorem for the Generalized Lambek Calculus. We use a Labelled Deductive System which generalizes the one used by Buszkowski [4] and Pankrat'ev [17] in completeness theorems for the Lambek Calculus.

We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".

Tarski’s conceptual analysis of the notion of logical consequence is one of the pinnacles of the process of defining the metamathematical foundations of mathematics in the tradition of his predecessors Euclid, Frege, Russell and Hilbert, and his contemporaries Carnap, Gödel, Gentzen and Turing. However, he also notes that in defining the concept of consequence “efforts were made to adhere to the common usage of the language of every day life.” This paper addresses the issue of what relationship Tarski’s analysis, and (...) Béziau’s further generalization of it in universal logic, have to reasoning in the everyday lives of ordinary people from the cognitive processes of children through to those of specialists in the empirical and deductive sciences. It surveys a selection of relevant research in a range of disciplines providing theoretical and empirical studies of human reasoning, discusses the value of adopting a universal logic perspective, answers the questions posed in the call for this special issue, and suggests some specific research challenges. (shrink)

In this paper we consider the relations existing between four deductive systems that have been called categorial grammars and have relevant connections with linguistic investigations: the syntactic calculus, bilinear logic, compact bilinear logic and Curry''s semantic calculus.

We discuss the logic of pregroups, introduced by Lambek [34], and its connections with other type logics and formal grammars. The paper contains some new ideas and results: the cut-elimination theorem and a normalization theorem for an extended system of this logic, its P-TIME decidability, its interpretation in L1, and a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid.

This work addresses biological explanations and aims to provide a philosophical account which brings together logical-procedural and historical-processual aspects when considering molecular pathways. It is argued that, having molecular features as explananda, a particular non-classical logical language – Zsyntax – can be used to formally represent, in terms of logical theorems, types of molecular processes, and to grasp how we get from one molecular interaction to another, hence explaining why a given outcome occurs. Expressing types of molecular biology processes in (...) terms of the Zsyntax language allows us to represent causal interactions by taking into account their context-sensitivity, and amounts to partly reviving the spirit of the so-called received view of explanation – which aimed to capture scientific explanatory accounts in terms of their logical structure and their appealing to nomological relations. Such a partial revival is pursued by invoking here non-classical deductions and empirical generalisations, which are called to provide the epistemic norms to explain the behavior of molecular pathways. (shrink)

This paper briefly overviews some of the results and research directions. In the area of substructural logics from the last couple of decades. Substructural logics are understood here to include relevance logics, linear logic, variants of Lambek calculi and some other logics that are motivated by the idea of omitting some structural rules or making other structural changes in LK, the original sequent calculus for classical logic.

The seminal book on graph theory by Dénes Kőnig, published in the year 1936, collected notions and results from precursory works from the mid to late nineteenth century by Hamilton, Cayley, Sylvester and others. More importantly, Kőnig himself contributed many of his own results that he had obtained in the more than twenty years that he had been working on this subject matter. What is noteworthy is the fact that the fundamentals of what he calls directed graphs are taken almost (...) exhaustively from Paul Hertz' 1922 article on structural reasoning about sentences of the form a→b. This is not a fact that is well known in logical circles, even though Kőnig fully acknowledges this in his book. In view of the numerous trends in the recent decades to describe and explicate logical matters by means of graphs, the fact that it was Hertz' foundation of structural reasoning that informed basic notions of graph theory in the first place is highly significant. The main goal of this paper is to summarize Hertz' article and demonstrate how Kőnig integrates the notions and results presented therein in his book. This is followed by an exposition of how and when Hertz' results were reinvented in terms of graph theory. A critical discussion of the opinion expressed by both Hertz and Kőnig that the more general sentences of the form (a1,…,an)→b, introduced by Hertz in a companion article in 1923, cannot be interpreted by graphs concludes this paper. (shrink)

summary of work in relevant in the Anderson– tradition.]; Mares Troestra, Anne, 1992, Lectures on , CSLI Publications [A quick, easy-to.

Inferentialism is the conviction that to be meaningful in the distinctively human way, or to have a 'conceptual content', is to be governed by a certain kind of inferential rules. The term was coined by Robert Brandom as a label for his theory of language; however, it is also naturally applicable (and is growing increasingly common) within the philosophy of logic.