In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality (...) of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination. (shrink)

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into (...) a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

Focused sequent calculi are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document} for Lambek–Grishin logic by generalizing the theory of multi-type calculi (...) and their algebraic semantics with heterogenous consequence relations. The calculus fD.LG has strong focalization and it is sound and complete w.r.t. FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document}. This completeness result is in a sense stronger than completeness with respect to standard polarized algebraic semantics, insofar as we do not need to quotient over proofs with consecutive applications of shifts over the same formula. We also show a number of additional results. fD.LG is sound and complete w.r.t. LG-algebras: this amounts to a semantic proof of the so-called completeness of focusing, given that the standard (display) sequent calculus for Lambek–Grishin logic is complete w.r.t. LG-algebras. fD.LG and the focused calculus fLG of Moortgat and Moot are equivalent with respect to proofs, indeed there is an effective translation from fLG-derivations to fD.LG-derivations and vice versa: this provides the link with operational semantics, given that every fLG-derivation is in a Curry–Howard correspondence with a directional λ¯μμ~\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\overline{\lambda }\mu \widetilde{\mu }$$\end{document}-term. (shrink)

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show how to constrain applications of display-equivalence in our calculi in such a way that an exhaustive proof search need be only finitely branching, and establish a full deduction theorem for the bunched logics with classical additives, (...) BBI and CBI. We also show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic are very unlikely to exist. (shrink)

We extend Takuro Onishi’s result on displaying substructural negations by formulating display calculi for non-normal versions of impossibility and unnecessity operators, called regular and co-regular negations, respectively, by Dimiter Vakarelov. We make a number of connections between Onishi’s work and Vakarelov’s study of negation. We also prove a decidability result for our display calculus, which can be naturally extended to obtain decidability results for a large number of display calculi for logics with negative modal operators.

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)

In this essay I give a complete join semi-lattice of possible display-equivalence schemes for Display Logic, using the standard connectives, and leaving fixed only the schemes governing the star. In addition to proving the completeness of this list, I offer a discussion of the basic properties of these schemes.

We use a deep embedding of the display calculus for relation algebras RA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for RA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle /HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle /HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

In this paper we introduce and compare four different syntactic methods for generating sequent calculi for the main systems of modal logic: the multiple sequents method, the higher-arity sequents method, the tree-hypersequents method and the display method. More precisely we show how the first three methods can all be translated in the fourth one. This result sheds new light on these generalisations of the sequent calculus and raises issues that will be examined in the last section.

We compare several methods of implementing the display (sequent) calculus RA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for RA and any associated increase in proof length. We discuss issues arising from this requirement.

The paper presents the diagrammatic calculus CL, which combines features of tree, Euler-type, Venn-type diagrams and squares of opposition. In its basic form, `CL' (= Cubus Logicus) organizes terms in the form of a square or cube. By applying the arrows of the square of opposition to CL, judgments and inferences can be displayed. Thus CL offers on the one hand an intuitive method to display ontologies and on the other hand a diagrammatic tool to check inferences. The (...) paper focuses mainly on the adaptation of the square of opposition in CL and offers an algebraic notation, which corresponds to the diagrammatic representation. (shrink)

The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer context-sensitive. (...) A recipe for characterizing structural extensions of display calculi is provided. (shrink)

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural (...) deduction system of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

We, the authors, would like to thank Guillaume Aucher for informing us of his “Displaying Updates in Logic”, published in the Journal of Logic and Computation, 26:1865-1912.

In this paper we study numeral systems in the -calculus. With one exception, we assume that all numerals have normal form. We study the independence of the conditions of adequacy of numeral systems. We find that, to a great extent, they are mutually independent. We then consider particular examples of numeral systems, some of which display paradoxical properties. One of these systems furnishes a counterexample to a conjecture of Böhm. Next, we turn to the approach of Curry, Hindley, (...) and Seldin. We dwell with the general problem of obtaining their results with the additional requirement of nonconvertibility of numerals. In particular we solve a problem that they left open. Finally, we give the first example of an adequate unsolvable numeral system without a test for zero in the usual sense, thus solving a problem of Barendregt and Barendsen. (shrink)

A new combined temporal logic called synchronized linear-time temporal logic (SLTL) is introduced as a Gentzen-type sequent calculus. SLTL can represent the n -Cartesian product of the set of natural numbers. The cut-elimination and completeness theorems for SLTL are proved. Moreover, a display sequent calculus δ SLTL is defined.

A theory of substructural negations as impossibility and as unnecessity based on bi-intuitionistic logic, also known as Heyting-Brouwer logic, has been developed by Takuro Onishi. He notes two problems for that theory and offers the identification of the two negations as a solution to both problems. The first problem is the lack of a structural rule corresponding with double negation elimination for negation as impossibility, DNE, and the second problem is a lack of correspondence between certain sequents and a characterizing (...) frame property. While the identification of negation as impossibility and negation as unnecessity does solve Onishi’s problems, in general it nevertheless seems desirable to keep the two notions separate. The present paper addresses the first problem by introducing a reformulation of Onishi’s display sequent calculus in a language of sequents that incorporates Boolean negation. Instead of identifying negation as impossibility and negation as unnecessity, a notion of weak frame correspondence is defined. It is observed that DNE weakly corresponds with a certain frame property, and two structural sequent rules are presented that together also weakly correspond with that frame property and allow one to derive DNE. Moreover, the reformulated display calculus has an independent motivation by considerations on proof-theoretic semantics. (shrink)

This paper deals with the question of the logicality of modal logics from a proof-theoretic perspective. It is argued that if Dos̆en’s analysis of logical constants as punctuation marks is embraced, it is possible to show that all the modalities in the cube of normal modal logics are indeed logical constants. It will be proved that the display calculus for each displayable modality admits a purely structural presentation based on double-line rules which, following Dos̆en’s analysis, allows us to (...) claim that the corresponding modal operators are logical constants. (shrink)

We present substructural negations, a family of negations classified in terms of structural rules of an extended kind of sequent calculus, display calculus. In considering the whole picture, we emphasize the duality of negation. Two types of negative modality, impossibility and unnecessity, are discussed and "self-dual" negations like Classical, De Morgan, or Ockham negation are redefined as the fusions of two negative modalities. We also consider how to identify, using intuitionistic and dual intuitionistic negations, two accessibility relations (...) associated with impossibility and unnecessity. (shrink)

This thesis provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. After an illustration of the basic principles of proof-theoretic semantics, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reject on them in the light of proof-theoretic semantic principles. The main original contributions of the present thesis are: (a) a revised version of the display-style calculus D.EAK, which we argue (...) to be more adequate from the proof-theoretic semantic viewpoint; the main feature of this revision is that a smoother proof (so-called Belnap-style) of cut-elimination holds for it, which is problematic for the original version of D.EAK. (b) The intro duction of a novel, multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The presence of types endows the language of the Dynamic Calculus with additional expressivity, and makes it possible to design rules with an even smoother behavior. We argue that this calculus paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly for proof systems beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination. (shrink)

This paper discusses a generalization of logical expressivism. It is shown that, in the wide sense defined here, the expressivist approach is neutral with respect to different theories of inference and offers a natural framework for understanding logical forms and their function. An expressivist strategy for explaining the development of logical forms is then applied to the analysis of Frege’s Begriffsschrift, Gentzen’s sequent calculus and Belnap’s display logic.

A star-free relational semantics for relevant logic is presented together with a sound and complete sequent proof theory. It is an extension of the dualist approach to negation regarded as modality, according to which de Morgan negation in relevant logic is better understood as the confusion of two negative modalities. The present work shows a way to define them in terms of implication and a new connective, co-implication, which is modeled by respective ternary relations. The defined negations are confused by (...) a special constraint on ternary relation, called the generalized star postulate, which implies definability of the Routley star in the frame. The resultant logic is shown to be equivalent to the well-known relevant logic R. Thus it can be seen as a reconstruction of R in the dualist framework. (shrink)

Fodor advocates a view of cognitive processes as computations defined over the language of thought (or Mentalese). Even among those who endorse Mentalese, considerable controversy surrounds its representational format. What semantically relevant structure should scientific psychology attribute to Mentalese symbols? Researchers commonly emphasize logical structure, akin to that displayed by predicate calculus sentences. To counteract this tendency, I discuss computational models of navigation drawn from probabilistic robotics. These models involve computations defined over cognitive maps, which have geometric rather than (...) logical structure. They thereby demonstrate the possibility of rational cognitive processes in an exclusively non-logical representational medium. Furthermore, they offer much promise for the empirical study of animal navigation. (shrink)

In this paper I will show the problems that are encountered when dealing with uniqueness of connectives in a bilateralist setting within the larger framework of proof-theoretic semantics and suggest a solution. Therefore, the logic 2Int is suitable, for which I introduce a sequent calculus system, displaying - just like the corresponding natural deduction system - a consequence relation for provability as well as one dual to provability. I will propose a modified characterization of uniqueness incorporating such a duality (...) of consequence relations, with which we can maintain uniqueness in a bilateralist setting. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

Quite often the compatibility of the EPR correlations with the relativity theory has been questioned; it has been stated that “the first in time of two correlated measurements instantaneously collapses the other subsystem”; it has been suggested that a causal asymmetry is built into the Feynman propagator. However, the EPR transition amplitude, as derived from the S matrix, is Lorentz andCPT invariant; the correlation formula is symmetric in the two measurements irrespective of their time ordering, so that the link of (...) the correlations is the Feynman zigzag, and that causality isCPT invariant at the microlevel; finally, although the Feynman propagator has theP andCT symmetries, no causal asymmetry follows from that. As for Stapp's views concerning “process” and “becoming,” and his Whiteheadean concept of an advancing front, I object that they belong to “factlike macrophysics,” and are refuted at the microlevel by the EPR phenomenology, which displays direct Fokker-like space-time connections. The reason for this is a radical one. The very blending of a space-time picture and of a probability calculus is a paradox. The only adequate paradigm is one denying objectivity to space-time—but this, of course, is also required by the complementary of the x and the k pictures, which only “look” compatible at the macrolevel. Therefore, the classical “objectivity” must yield in favor of “intersubjectivity.” Only the macroscopic preparing and measuring devices have “factlike” objectivity; the “transition” of the “quantal system” takes place beyond both thex and thek 4-spaces. Then, the intrinsic symmetries between retarded and advanced waves, and statistical prediction and retrodiction, entails that the future has no less (but no more) existence than the past. It is the future that is significant in “creative process,” the “elementary” forms of which should be termed “precognition” or “psychokinesis”—respectively symmetric to the factlike taboos that “we can neither know into the future nor act into the past.” It is gratifying that Robert Jahn, at the Engineering School of Princeton University, is conducting (after others) conclusive experiments demonstrating “low level psychokinesis”—a phenomenon implied by the very symmetry of the negentropy-information transition. So, what pierces the veil of “maya” is the (rare) occurrence of “paranormal phenomena.” The essential severance between “act” and “potentia” is not a spacelike advancing front, but the “out of” and the “into” factlike space-time. Finally, I do not feel that an adequate understanding of the EPR phenomenology requires going beyond the present status of relativistic quantum mechanics. Rather, I believe that the potentialities of this formalism have not yet been fully exploited. (shrink)

The distinction between the proofs that only certify the truth of their conclusion and those that also display the reasons why their conclusion holds has a long philosophical history. In the contemporary literature, the grounding relation—an objective, explanatory relation which is tightly connected with the notion of reason—is receiving considerable attention in several fields of philosophy. While much work is being devoted to characterising logical grounding in terms of deduction rules, no in-depth study focusing on the difference between grounding (...) rules and logical rules exists. In this work, we analyse the relation between logical grounding and classical logic by focusing on the technical and conceptual differences that distinguish grounding rules and logical rules. The calculus employed to conduct the analysis provides moreover a strong confirmation of the fact that grounding derivations are logical derivations of a certain kind, without trivialising the distinction between grounding and logical rules, explanatory and non-explanatory parts of a derivation. By a further formal analysis, we negatively answer the question concerning the possible correspondence between grounding rules and intuitionistic logical rules. (shrink)

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display (...) calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem. (shrink)

We formally investigate immediate and mediate grounding operators from an inferential perspective. We discuss the differences in behaviour displayed by several grounding operators and consider a general distinction between grounding and logical operators. Without fixing a particular notion of grounding or grounding relation, we present inferential rules that define, once a base grounding calculus has been fixed, three grounding operators: an operator for immediate grounding, one for mediate grounding – corresponding to the transitive closure of the immediate grounding one (...) – and a grounding tree operator, which enables us to internalise chains of immediate grounding claims without losing any information about them. We then present an in-depth proof-theoretical study of the introduced rules by focussing, in particular, on the question whether grounding operators can be considered as logical operators and whether balanced rules for grounding operators can be defined. (shrink)

A simple indeterministic system is displayed and it is urged that we cannot responsibly infer inductively over it if we presume that the probability calculus is the appropriate logic of induction. The example illustrates the general thesis of a material theory of induction, that the logic appropriate to a particular domain is determined by the facts that prevail there.

Paradox is a logical phenomenon. Usually, it is produced in type theory, on a type Ω of “truth values”. A formula Ψ (i.e., a term of type Ω) is presented, such that Ψ↔¬Ψ (with negation as a term¬∶Ω→Ω)-whereupon everything can be proved: In Sect. 1 we describe a general pattern which many constructions of the formula Ψ follow: for example, the well known arguments of Cantor, Russell, and Gödel. The structure uncovered behind these paradoxes is generalized in Sect. 2. This (...) allows us to show that Reynolds' [R] construction of a typeA ≃℘℘A in polymorphic λ-calculus cannot be extended, as conjectured, to give a fixed point ofevery variable type derived from the exponentiation: for some (contravariant) types, such a fixed point causes a paradox.Pursueing the idea that $$\frac{{{\text{type theory}}}}{{{\text{categorical interpretation}}}} = \frac{{{\text{(propositional) logic}}}}{{{\text{Lindebaum algebra}}}}$$ the language of categories appears here as a natural medium for logical structures. It allows us to abstract from the specific predicates that appear in particular paradoxes, and to display the underlying constructions in “pure state”. The essential role of cartesian closed categories in this context has been pointed out in [L]. The paradoxes studied here remain within the limits of the cartesian closed structure of types, as sketched in this Lawvere's seminal paper — and do not depend on any logical operations on the type Ω. Our results can be translated in simply typed λ-calculus in a straightforward way (although some of them do become a bit messy). (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:Logos and Alogon: Thinkable and Unthinkable in Mathematics, from the Pythagoreans to the Moderns by Arkady PlotnitskyNoam CohenPLOTNITSKY, Arkady. Logos and Alogon: Thinkable and Unthinkable in Mathematics, from the Pythagoreans to the Moderns. Cham: Springer, 2023. xvi + 294 pp. Cloth, $109.99The limits of thought in its relations to reality have defined Western philosophical inquiry from its very beginnings. The shocking discovery of the incommensurables in Greek mathematics (...) not only reintroduced these limits with greater force but also instigated two different forms of coping with the unthinkable in Western philosophy, mathematics, and science. As Arkady Plotnitsky sets forth, in response to the incommensurability crisis in the ancient Greek intellectual world, there appeared two different attitudes toward the alogon, that is, the unthinkable or irrational. Plato and his followers sought to overcome the unthinkable, of which the incommensurables in mathematics are only an example, through philosophy. In contrast, the Pythagoreans continued to hold on to mathematics as the primary means of knowing the world, but put a larger emphasis on geometry. Plotnitsky [End Page 359] claims that by not putting aside the primacy of mathematics, the Pythagorean shift from arithmetic to geometry established in Western thought a certain tolerance toward the unthinkable within the realm of the thinkable, “a possibility of the alogon in the logos.” Until modern times this remained no more than a possibility. However, in modern mathematics and mathematical physics Plotnitsky identifies a certain fulfillment of this potential, a “radical Pythagorean mathematics.” In his comprehensive and thought-provoking study, Plotnitsky recounts the development of such radical modern Pythagoreanism, not only to tell its history but also to suggest that the unthinkable is a condition of possibility for thought, and that a proper recognition of this role it plays is crucial for the advancement of mathematical thinking and thinking in general.Plotnitsky begins by portraying in broad strokes the two defining characteristics of radical Pythagorean mathematics: the presence of the unthinkable within mathematical thought itself, and the interplay of algebra and geometry. Relying on an extensive knowledge of the history of modern mathematics and physics, in the first two chapters of the book Plotnitsky gradually demonstrates the key role that the alogon plays in some theories of modern mathematical thought, such as Gödel’s incompleteness theorems and quantum mechanics. He also presents and clarifies his own conception of the history of Western thought as a creative process of concept-forming. By creating rather than discovering concepts, great mathematicians break new ground for thinking. The book as a whole argues in length for these two main theses.In chapter 3, the author addresses the thought of Bernhard Riemann to make the case that Riemann’s mathematical thought puts an emphasis on creative conceptual thinking and is not defined merely by calculations or logic. Such thinking is problem-posing rather than axiomatic. Riemann’s central innovation in this respect is the concept of manifold (Mannigfaltigkeit), which enabled him to think anew space and geometry in a radical non-Euclidean fashion, implying an infinite number of possible geometries. Plotnitsky argues—borrowing Deleuze and Guattari’s terminology—that this opened up a “plane of immanence,” which is to say that Riemann created a concept-generating movement of thought. However, we cannot grasp the generation of concepts in modern mathematics without giving proper attention to the interplay of algebra and geometry that defines it. Chapter 4 demonstrates this interweaving of the two fields by recounting the history of the idea of the curve in modernity, from the analytic geometry and calculus of Fermat and Descartes to its modification in the concept of a Riemann surface, up to its more recent developments in the algebraic geometry of Weil and Grothendieck. It gives a historical account of the algebraization of the curve that at the same time brings into relief the irreducible geometrical aspect, continuity, of all modern mathematical conceptualizations of the curve.The next two chapters provide further case studies. Chapter 5 expands and solidifies the argument of chapter 2. It discusses three examples of mathematical practice, each displayed by a pair of important [End Page 360] mathematicians: Abel and Galois, Lobachevsky and Riemann, Weil and Grothendieck. Each case... (shrink)

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived (...) calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

Online social networks (OSN) have become a part of our daily lives whether they are used for socialization and communication or to promote business interests. OSN have become an important tool for businesses to advertise, create brand awareness, and promote their products and services. Business use of OSN for advertising purposes is highly reliant on targeted ads which display advertisements to OSN users based on their demographics and use of OSN, apps, and websites. Thus, one of the most valuable (...) commodities of OSN is the population of users and the information they share. To investigate the relationship between OSN site use, use of privacy settings, and how they relate to profile disclosure, a model is built based on the theory of reasoned action and the privacy calculus model. To validate the model, a survey is conducted and the results are analyzed with partial least squares. Risk and benefit were both shown to be significant antecedents of attitude. Both attitude and subjective norm, from the theory of reasoned action model, significantly affected OSN site use, while omitting intentions. OSN site use was significantly related to both profile disclosure and use of privacy settings. Last, use of privacy settings significantly affected profile disclosure. These results imply that use of privacy settings does not decrease the rate of disclosure. Giving users tools to protect their private information is important in protecting the privacy of OSN users, and it will lead to increases in safe disclosure of information helping OSN target ads effectively. (shrink)

Four consequence operators based on hypergraph satisfiability are defined. Their properties are explored and interconnections are displayed. Finally their relation to the case of the Classical Propositional Calculus is shown.

The editors of the Applied Logic Series are happy to present to the reader the fifth volume in the series, a collection of papers on Logic, Language and Computation. One very striking feature of the application of logic to language and to computation is that it requires the combination, the integration and the use of many diverse systems and methodologies - all in the same single application. The papers in this volume will give the reader a glimpse into the problems (...) of this active frontier of logic. The Editors CONTENTS Preface IX 1. S. AKAMA Recent Issues in Logic, Language and Computation 1 2. M. J. CRESSWELL Restricted Quantification 27 3. B. H. SLATER The Epsilon Calculus' Problematic 39 4. K. VON HEUSINGER Definite Descriptions and Choice Functions 61 5. N. ASHER Spatio-Temporal Structure in Text 93 6. Y. NAKAYAMA DRT and Many-Valued Logics 131 7. S. AKAMA On Constructive Modality 143 8. H. W ANSING Displaying as Temporalizing: Sequent Systems for Subintuitionistic Logics 159 9. L. FARINAS DEL CERRO AND V. LUGARDON 179 Quantification and Dependence Logics 10. R. SYLVAN Relevant Conditionals, and Relevant Application Thereof 191 Index 245 Preface This is a collection of papers by distinguished researchers on Logic, Lin guistics, Philosophy and Computer Science. The aim of this book is to address a broad picture of the recent research on related areas. In particular, the contributions focus on natural language semantics and non-classical logics from different viewpoints. (shrink)

The paper consists of two parts. The first part begins with the problem of whether the original three-valued calculus, invented by J. Łukasiewicz, really conforms to his philosophical and semantic intuitions. I claim that one of the basic semantic assumptions underlying Łukasiewicz's three-valued logic should be that if under any possible circumstances a sentence of the form "X will be the case at time t" is true (resp. false) at time t, then this sentence must be already true (resp. (...) false) at present. However, it is easy to see that this principle is violated in Lukasiewicz's original calculus (as the cases of the law of excluded middle and the law of contradiction show). Nevertheless it is possible to construct (either with the help of the notion of "supervaluation", or purely algebraically) a different three-valued, semi-classical sentential calculus, which would properly incorporate Łukasiewicz's initial intuitions. Algebraically, this calculus has the ordinary Boolean structure, and therefore it retains all classically valid formulas. Yet because possible valuations are no longer represented by ultrafilters, but by filters (not necessarily maximal), the new calculus displays certain non-classical metalogical features (like, for example, nonextensionality and the lack of the metalogical rule enabling one to derive "p is true or q is true" from" 'p ∨ q' is true"). The second part analyses whether the proposed calculus could be useful in formalizing inferences in situations, when for some reason (epistemological or ontological) our knowledge of certain facts is subject to limitation. Special attention should be paid to the possibility of employing this calculus to the case of quantum mechanics. I am going to compare it with standard non-Boolean quantum logic (in the Jauch-Piron approach), and to show that certain shortcomings of the latter can be avoided in the former. For example, I will argue that in order to properly account for quantum features of microphysics, we do not need to drop the law of distributivity. Also the idea of "reading off" the logical structure of propositions from the structure of Hilbert space leads to some conceptual troubles, which I am going to point out. The thesis of the paper is that all we need to speak about quantum reality can be acquired by dropping the principle of bivalence and extensionality, while accepting all classically valid formulas. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Journal of the History of Philosophy 41.3 (2003) 416-417 [Access article in PDF] Jean-Baptiste Rauzy. La Doctrine leibnizienne de la vérité. Aspects logiques et ontologiques. Paris: Vrin, 2001. Pp. vii + 353. Paper, FF 170,55.This important book provides a reappraisal of Leibniz's philosophy of logic and epistemology based on a close scrutiny of the recently edited manuscripts in the Akademie-Ausgabe, and a reconstitution of Leibniz's sequential investigations. The author (...) displays an exceptional knowledge of the Leibnizian corpus, the ancient and medieval sources for the various doctrines he analyzes, and the contemporary issues underpinning Leibniz's investigations. He aims at rectifying misconceptions that stemmed originally in Couturat's La Logique de Leibniz (1901) and have since affected several studies. Three methodological statements set the ground for Rauzy's analysis: (1) Leibniz's notion of truth concerns in unified fashion all the elements of discourse: terms, concepts, and propositions. (2) Leibniz did not restrict his doctrine of truth to consistency relations, but yielded a complex, well-articulated conception of truth as correspondence, as evidenced in New Essays on Human Understanding, IV, v, sect. 11; yet, at the same time, his doctrine focused on conceptual relations which specify an order of reasons deserving to be analyzed for their own sake: "Dans la doctrine leibnizienne de la vérité, l'adaequatio rei constitue encore le cadre général en dehors duquel le prédicat de vérité n'a pas de sens. Mais les concepts et les liaisons conceptuelles donnent désormais la raison pour laquelle telle phrase particulière est vraie..." (47). And (3) one should resist attributing to Leibniz a purely syntactic conception of truth since the semantic dimension of his logical analyses deserves to be reconstituted and due consideration should be given to the evolution of his thoughts on central philosophical issues, which occasioned significant variations in the elements and formulas of his calculus rationis.It is merely possible to render the rich contents of the book by mentioning some of its more striking features. In Chapter 1, the inesse principle (Praedicatum inestsubjecto) is shown to serve grammatical, logical, and conceptual functions. The doctrine of expression is finely analyzed: expression is shown to provide the major translation tool between characters and thoughts and to condition the combinatorial treatment of rational discourse. In Chapter 2, the distinction between concept and object is shown to involve some relativity, even if the understanding of complete notions is supposed to entail real knowledge of the corresponding realities. Leibniz is thus justified to represent the manifold of ontological relations, including the requisites of actual existence, in a tentatively unified logical way: "Que [End Page 416] l'existence soit une propriété relationnelle complexe, conçue tantôt par la relation de compatibilité, tantôt par une relation à l'esprit en général—et éventuellement [...] par un mixte des deux—n'interdit nullement de maintenir que la vérité de toutes les propositions dépend de relations conceptuelles" (124-5). In Chapter 3, the project of a calculus based on concepts is shown to entail a special relation, hardly dealt with in the literature, between intension and extension (cf. for instance New Essays, IV, xvii, sect. 8). Rauzy reassesses in particular Leibniz's critical revision of nominalism and of inductive procedures as these require universal propositions to ground rational presumptions. The extensional notion of class is considered an abstraction: a class presupposes therefore the extension of a concept in order to become an object of thought. The principle of conceptual inherence requires to be interpreted as stating the equipollence between the requisites of subject and predicate; if such an equipollence may be reached a priori in exceptional cases, most of the time it will require various kinds of additions and derivations to yield sufficient congruence between the related terms. Chapter 4 is devoted to substitutions, more precisely to the theory of definition and the context, at once logical and discursive, from which a potential Leibnizian theory of communication might be derived. Rauzy notes that substitutive equivalences... (shrink)

Paraconsistent extensions of 3-valued Gödel logic are studied as tools for knowledge representation and nonmonotonic reasoning. Particularly, Osorio and his collaborators showed that some of these logics can be used to express interesting nonmonotonic semantics. CG’3 is one of these 3-valued logics. In this paper, we introduce Fidel semantics for a certain calculus of CG’3 by means of Fidel structures, named CG’3-structures. These structures are constructed from enriched Boolean algebras with a special family of sets. Moreover, we also show (...) that the most basic CG’3-structures coincide with da Costa–Alves’ bi-valuation semantics; this connection is displayed through a Representation Theorem for CG’3-structures. By contrast, we show that for other paraconsistent logics that allow us to present semantics through Fidel structures, this connection is not held. Finally, Fidel semantics for the first-order version of the logic of CG’3 are presented by means of adapting algebraic tools. (shrink)

In General Inquiries on the Analysis of Notions and Truths, Leibniz articulates for the first time his favourite solution to the problem of contingency and displays the main features of his logical calculus. Leibniz composed the work in 1686, the same year in which he began to correspond with Arnauld and wrote the Discourse on Metaphysics. General Inquiries supplements these contemporary entries in Leibniz's philosophical oeuvre and demonstrates the intimate connection that links Leibniz's philosophy with the attempt to create (...) a new kind of logic. This edition presents the text and translation of the General Inquiries along with an introduction and commentary. Given the composite structure of the text, where logic and metaphysics strongly intertwine, Mugnai's introduction falls into two sections, respectively dedicated to logic and metaphysics. The first section ('Logic') begins with a preliminary account of Leibniz's project for a universal characteristic and focuses on the relationships between rational grammar and logic, and discusses the general structure and the main ingredients of Leibniz's logical calculus. The second section ('Metaphysics') is centred on the problem of contingency, which occupied Leibniz until the end of his life. Mugnai provides an account of the problem, and details Leibniz's proposed solution, based on the concept of infinite analysis. (shrink)

Thus far the logic out of which mathematics has developed has been First-order Predicate Calculus with Identity, that is the logic of the sentential functors, ¬, →, ∧, ∨, etc., together with identity and the existential and universal quotifiers restricted to quotify- ing only over individuals, and not anything else, such as qualities or quotities themselves. Some philosophers—among them Quine— have held that this, First-order Logic, as it is often called, con- stitutes the whole of logic. But that is (...) a mistake. It leaves out Second-order Logic, which we need if we are to characterize the natural numbers precisely, and pays scant attention to the logic of relations, especially transitive relations, which is the key to much of modern mathematics. Quine’s argument for restricting logic to First-order Logice was based on the grounds that only First- order logical theories display “Law and Order” and himself regards modal logic as belonging with witchcraft and superstition.1 Pred- icates are ontologically more suspect than individuals, and have a different logic, which is liable to give rise to paradox and inconsis- tency. Moreover, Second-order Logic lacks the completeness that First-order Logice has, which provides a pleasing parallel between syntactic and semantic notions, and argues for the analyticity of deductive logic. (shrink)

In this article we describe the logical performances displayed by a context-dependent associative memory model. This model requires the existence of a network able to construct the Kroneker product of two vectors, and then to send the composed vector to a correlation distributed memory. This system of nets is capable to sustain all the operations of the classical propositional calculus. This fact implies the existence of vector logics where the logical functions are displayed by matrix operators constructed using the (...) properties of the Kronecker product. When the basic binary matrix operators act on fuzzy inputs, a probabilistic many-valued logic emerges. The present approach implies the potential existence of alternative vector logics. We describe a vector Shefferian “Iogic”, and we comment the potentialities of multidimensional vector logics. (shrink)

1. ExpositionRichard Sharvy's ‘A more general theory of definite descriptions’ was published in 1980. Its aim was to replace Russell's paradigm by " a general theory of definite descriptions, of which definite mass descriptions, definite plural descriptions, and Russellian definite singular count descriptions are species. … We have an account of the generic ‘the’ along these same lines. " By now his theory has attained the status of a new paradigm. Even a casual trawl of the literature throws up over (...) a score of citations and endorsements, and no rebuttals of its central contention that the primary use of ‘the’ is to indicate totality . We shall argue that it is wrong for mass description, wrong for singular description, wrong for plural description and wrong for generic ‘the’. Sharvy would have approved: his obituary says that his car displayed the slogan ‘Subvert the Dominant Paradigm’.He follows Russell in treating descriptions as incomplete symbols, but nothing in his paper turns on this aspect of it, and we can bypass the issue by considering them in the context of complete sentences. Where Russell translates F into the predicate calculus as Formula Sharvy translates it as Formula Here ≤ is supposed to stand for some or other species of part of relation. His other governing idea is of a predicate's being cumulative. G is cumulative if any number of things that satisfy G have a sum, i.e. a least upper bound with respect to ≤ which also satisfies G. The meanings of ≤, sum and cumulativity vary according to the different kinds of description, which we take in the order in which Sharvy presents them. Meanwhile, we note that he originally defined ‘sum’ to mean simply the l.u.b. , but subsequently redefined …. (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.