A dialetheia is a sentence, A, such that both it and its negation, A, are true (we shall talk of sentences throughout this entry; but one could run the definition in terms of propositions, statements, or whatever one takes as her favourite truth bearer: this would make little difference in the context). Assuming the fairly uncontroversial view that falsity just is the truth of negation, it can equally be claimed that a dialetheia is a sentence which is both true and (...) false. (shrink)

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)

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.

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)

A dialetheia is a sentence, A, such that both it and its negation, ¬A, are true (we shall talk of sentences throughout this entry; but one could run the definition in terms of propositions, statements, or whatever one takes as her favourite truth-bearer: this would make little difference in the context). Assuming the fairly uncontroversial view that falsity just is the truth of negation, it can equally be claimed that a dialetheia is a sentence which is both true and false.

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.

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 consider the task of theorem proving in Lambek calculi and their generalisation to ‘multimodal residuation calculi’. These form an integral part of categorial logic, a logic of signs stemming from categorial grammar, of the basis of which language processing is essentially theorem proving. The demand of this application is not just for efficient processing of some or other specific calculus, but for methods that will be generally applicable to categorial logics.It is proposed that multimodal cases be treated by dealing (...) with the highest common factor of all the connectives as linear validity. The prosodic aspects are encoded in labels, in effect the term-structure of quantified linear logic. The correctness condition on proof nets can be implemented by SLD resolution in linear logic with unification on labels/terms limited to one way matching. A suitable unification strategy is obtained for calculi of discontinuity by normalisation of the ground goal term followed by recursive descent and redex pattern matching on the head term. (shrink)

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".

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)

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.

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)

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)

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)

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.

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.

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)