Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime (...) complexity of the multiplicative fragment of NBL. (shrink)

We present a method that generates two-sided sequent calculi for four-valued logics like "first degree entailment" (FDE). (We say that a logic is FDE-like if it has finitely many operators of finite arity, including negation, and if all of its operators are truth-functional over the four truth-values 'none', 'false', 'true', and 'both', where 'true' and 'both' are designated.) First, we show that for every n-ary operator * every truth table entry f*(x1,...,xn) = y can be characterized in (...) terms of a pair of sequent rules. Secondly, we use these sequent rules to build sequent calculi and prove their completeness. With the help of two simplification procedures we then show that the 2⋅4^n sequent rules that characterize an n-ary operator can be systematically reduced to at most four sequent rules. Thirdly, we use our method to investigate the proof-theoretical consequences of including intuitive truth-functional implications in FDE-like logics. (shrink)

In this paper we show that, in Gentzen systems, there is a close relation between two of the main characters in algebraic logic and proof theory respectively: protoalgebraicity and the cut rule. We give certain conditions under which a Gentzen system is protoalgebraic if and only if it possesses the cut rule. To obtain this equivalence, we limit our discussion to what we call regular sequent calculi, which are those comprising some of the structural rules and some logical (...) rules, in a sense we make precise. We note that this restricted set of rules includes all the usual rules in the literature. We also stress the difference between the case of two-sided sequents and the case of many-sided sequents, in which more conditions are needed. (shrink)

In [5] we study Nonassociative Lambek Calculus augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus. Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

Building on recent work, I present sequent systems for the non-classical logics LP, K3, and FDE with two main virtues. First, derivations closely resemble those in standard Gentzen-style systems. Second, the systems can be obtained by reformulating a classical system using nonstandard sequent structure and simply removing certain structural rules (relatives of exchange and contraction). I clarify two senses in which these logics count as “substructural.”.

ABSTRACT In this paper we study consequence relations on the set of many sided sequents over a propositional language. We deal with the consequence relations axiomatized by the sequent calculi defined in [2] and associated with arbitrary finite algebras. These consequence relations are examples of what we call Gentzen systems. We define a semantics for these systems and prove a Strong Completeness Theorem, which is an extension of the Completeness Theorem for provable sequents stated in (...) [2]. For the special case of the finite linear MV-algebras, the Strong Completeness Theorem was proved in [10], as a consequence of McNaughton's Theorem. The main tool to prove this result for arbitrary algebras is the deduction-detachment theorem for Gentzen systems. (shrink)

The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment (...) of a truth value and the exclusion of the opposite truth value describe the same situation.). (shrink)

A rejection system, also referred to as a complementary calculus, is a proof system axiomatising the invalid formulas of a logic, in contrast to traditional calculi which axiomatise the valid ones. Rejection systems therefore introduce a purely syntactic way of determining non-validity without having to consider countermodels, which can be useful in procedures for automated deduction and proof search. Rejection calculi have first been formally introduced by Łukasiewicz in the context of Aristotelian syllogistic and subsequently rejection systems for (...) many well-known logics have been proposed. In this paper, we deal with rejection systems for so-called non-deterministic finite-valued logics, a special case of non-deterministic many-valued logics which were introduced by Avron and Lev as a generalisation of traditional many-valued logics. More specifically, we introduce a systematic method for constructing sequent-style rejection systems for any given non-deterministic finite-valued logic. Furthermore, as special instances of our method, we provide concrete calculi for specific paraconsistent logics which can be characterised in terms of non-deterministic two- and three-valued semantics, respectively. (shrink)

In bilateral systems for classical logic, assertion and denial occur as primitive signs on formulas. Such systems lend themselves to an inferentialist story about how truth-conditional content of connectives can be determined by inference rules. In particular, for classical logic there is a bilateral proof system which has a property that Carnap in 1943 called categoricity. We show that categorical systems can be given for any finite many-valued logic using $n$-sided sequent calculus. These (...) class='Hi'>systems are understood as a further development of bilateralism—call it multilateralism. The overarching idea is that multilateral proof systems can incorporate the logic of a variety of denial speech acts. So against Frege we say that denial is not the negation of assertion and, with Mark Twain, that denial is more than a river in Egypt. (shrink)

Social enterprises are seen as innovative towards solving societal problems, but little research exists on possible negative aspects, the so‐called dark sides. In this study, the emphasis is on dark sides of social entrepreneurship, how they are managed, and how systems thinking can contribute towards managing these effects. Dark sides of social entrepreneurship can take many forms, like unethical or insincere motives and unintended outcomes like the negative impact on the well‐being of founders and employees, but they are (...) also a call for a critical reflection on the role of the government in society and the economic system social enterprises have to operate in. This paper aims to contribute to the dark side theory of social entrepreneurship by linking system archetypes to themes of dark side thereby stressing how management strategies act as balancing feedback loops to mitigate or prevent dark sides. A qualitative research was conducted by interviewing 21 respondents who play an important role in the world of social entrepreneurship in Belgium. The results show that dark sides of social enterprises manifest itself mostly in the form of trade‐offs and financial, business, and management related issues. Taking over the habits of profit‐oriented companies emerged as a new dark side element. Management strategies include anchoring goals, transparency, obtaining external views, changing the system, and above all reflection. The latter is an important first step to become aware of these issues to be able to change the negative dynamism of these dark sides. (shrink)

A wide family of many-valued logics—for instance, those based on the weak Kleene algebra—includes a non-classical truth-value that is ‘contaminating’ in the sense that whenever the value is assigned to a formula φ⁠, any complex formula in which φ appears is assigned that value as well. In such systems, the contaminating value enjoys a wide range of interpretations, suggesting scenarios in which more than one of these interpretations are called for. This calls for an evaluation of systems (...) with multiple contaminating values. In this paper, we consider the countably infinite family of multiple-conclusion consequence relations in which classical logic is enriched with one or more contaminating values whose behavior is determined by a linear ordering between them. We consider some motivations and applications for such systems and provide general characterizations for all consequence relations in this family. Finally, we provide sequent calculi for a pair of four-valued logics including two linearly ordered contaminating values before defining two-sided sequent calculi corresponding to each of the infinite family of many-valued logics studied in this paper. (shrink)

. The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves the (...) general structure of proofs in the original calculus in a way ensuring preservation of the weak cut elimination theorem under the transformation. The described transformation metod is illustrated on several concrete examples of many-valued logics, including a new application to information sources logics. (shrink)

Sequent calculi constitute an interesting and important category of proof systems. They are much less known than axiomatic systems or natural deduction systems are, and they are much less known than they should be. Sequent calculi were designed as a theoretical framework for investigations of logical consequence, and they live up to the expectations completely as an abundant source of meta-logical results. The goal of this book is to provide a fairly comprehensive view of (...) class='Hi'>sequent calculi -- including a wide range of variations. The focus is on sequent calculi for various non-classical logics, from intuitionistic logic to relevance logic, through linear and modal logics. A particular version of sequent calculi, the so-called consecution calculi, have seen important new developments in the last decade or so. The invention of new consecution calculi for various relevance logics allowed the last major open problem in the area of relevance logic to be solved positively: pure ticket entailment is decidable. An exposition of this result is included in chapter 9 together with further new decidability results (for less famous systems). A series of other results that were obtained by J. M. Dunn and me, or by me in the last decade or so, are also presented in various places in the book. Some of these results are slightly improved in their current presentation. Obviously, many calculi and several important theorems are not new. They are included here to ensure the completeness of the picture; their original formulations may be found in the referenced publications. This book contains very little about semantics, in general, and about the semantics of non-classical logic in particular. (shrink)

The paper contains an exposition of some non standard approach to gentzenization of modal logics. The first section is devoted to short discussion of desirable properties of Gentzen systems and the short review of various sequential systems for modal logics. Two non standard, cut-free sequent systems are then presented, both based on the idea of using special modal sequents, in addition to usual ones. First of them, GSC I is well suited for nonsymmetric modal logics The (...) second one, GSC II is devised specially for symmetric, i.e. Blogics. GSC I and GSC II are not different formalizations, from the theoretical point of view GSC I may be seen as a simplification of the more general approach present in GSC II. They are considered separately, mainly because Blogics demand different, and more complicated, strategy in completeness proof, whereas non symmetric logics are easily and uniformly characterised by means of Fitting's Consistency Properties. The weakest modal logic captured by this formalization is minimal regular logic C, but many stronger logics are obtainable by addition of suitable structural rules, which conforms to Do en's methodology. Both variants of GSC satisfy also other, besides cut-freedom, desirable properties. (shrink)

This reader collects and introduces important work in linguistics, computer science, artificial intelligence, and computational linguistics on the use of linguistic devices in natural languages to situate events in time: whether they are past, present, or future; whether they are real or hypothetical; when an event might have occurred, and how long it could have lasted. In focussing on the treatment and retrieval of time-based information it seeks to lay the foundation for temporally-aware natural language computer processing systems, for (...) example those that process documents on the worldwide web to answer questions or produce summaries. The development of such systems requires the application of technical knowledge from many different disciplines. The book is the first to bring these disciplines together, by means of classic and contemporary papers in four areas: tense, aspect, and event structure; temporal reasoning; the temporal structure of natural language discourse; and temporal annotation. Clear, self-contained editorial introductions to each area provide the necessary technical background for the non-specialist, explaining the underlying connections across disciplines.A wide range of students and professionals in academia and industry will value this book as an introduction and guide to a new and vital technology. The former include researchers, students, and teachers of natural language processing, linguistics, artificial intelligence, computational linguistics, computer science, information retrieval, library sciences, human-computer interaction, and cognitive science. Those in industry include corporate managers and researchers, software product developers, and engineers in information-intensive companies, such as on-line database and web-service providers. (shrink)

In this paper we develop what we can describe as a “dual two-sided” cut-free sequent calculus system for the non-classical logics of truth lp, k3, stt and a non-reflexive logic ts which is, arguably, more elegant than the three-sided sequent calculus developed by Ripley for the same logics. Its elegance stems from how it employs more or less the standard sequent calculus rules for the various connectives and truth, and the fact that it offers a (...) rather neat connection between derivable sequents and validity in comparison to the calculus developed by Ripley. (shrink)

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

Mereotopology is an extension of mereology with some relations of topological nature like contact. An algebraic counterpart of mereotopology is the notion of contact algebra which is a Boolean algebra whose elements are considered to denote spatial regions, extended with a binary relation of contact between regions. Although the language of contact algebra is quite expressive to define many useful mereological relations and mereotopological relations, there are, however, some interesting mereotopological relations which are not definable in it. Such are, (...) for instance, the relation of n-ary contact, internal connectedness and some others. To overcome this disadvantage, we introduce a generalisation of contact algebra, replacing the contact with a binary relation between finite sets of regions and a region, satisfying some formal properties of Tarski consequence relation. The obtained system is called sequent algebra, considered as an algebraic counterpart of a new mereotopology. We develop the topological representation theory for sequent algebras showing in this way certain correspondence between point-free and point-based models of space. As a by-product, we show how one logical relation in nature notion, Tarski consequence relation, may have also certain spatial meaning. (shrink)

The tetravalent modal logic is one of the two logics defined by Font and Rius :481–518, 2000) in connection with Monteiro’s tetravalent modal algebras. These logics are expansions of the well-known Belnap–Dunn’s four-valued logic that combine a many-valued character with a modal character. In fact, $${\mathcal {TML}}$$ TML is the logic that preserves degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $${\mathcal {TML}}$$ TML and the algebras is not (...) so good as in $${{\mathcal {TML}}}^N$$ TML N, but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus :481–518, 2000). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut-elimination property. Then, using a general method proposed by Avron et al., we provide a sequent calculus for $${\mathcal {TML}}$$ TML with the cut-elimination property. Finally, inspired by the latter, we present a natural deduction system, sound and complete with respect to the tetravalent modal logic. (shrink)

Publication date: 30 November 2016 Source: Author: Wen Lee Ng, Manimangai Mani, Wan Roselezam Wan Yahya While the growing body of research on Tan Twan Eng’s The Gift of Rain focuses on the protagonist, Philip Hutton’s traumatic condition, his Chinese identity, and his ambiguous identity, this study devotes particular attention to the complexity of interactions between various cultures practised by Philip. This study aims to address this gap by applying the concept of transculturalism to analyse the processes of acquiring a (...) foreign culture and incorporating the foreign culture into traditional cultures experienced by Philip. In other words, this study employs the concept of transculturalism to examine multicultural depictions in the novel. Scholars, such as Khan, Tiwari, Sheoran and Tan C. S. who have examined multicultural depictions in various literary texts, have found that multicultural circumstances cause certain ethnic groups to lose their cultures and identities. Hence, the multicultural circumstances depicted are perceived as negative phenomena. However, this study has found that by examining the interactions between various cultures, rather than focusing on the end products such as portrayals of hybridity, the positive sides of multicultural depictions could be revealed. The transculturation process experienced by Philip shows that the new cultural practices he has created are made up of both his traditional cultures and the foreign culture he has acquired. This means that Philip does not totally lose his traditional cultures and identities. Therefore, this study concludes that multicultural depictions in The Gift of Rain could be read positively, provided that the interactions between various cultures, which resulted in the incorporation of a foreign culture into traditional cultures, are examined. (shrink)

Since the outbreak of COVID-19, governments have turned their attention to digital contact tracing. In many countries, public debate has focused on the risks this technology poses to privacy, with advocates and experts sounding alarm bells about surveillance and mission creep reminiscent of the post 9/11 era. Yet, when Apple and Google launched their contact tracing API in April 2020, some of the world’s leading privacy experts applauded this initiative for its privacy-preserving technical specifications. In an interesting twist, the (...) tech giants came to be portrayed as greater champions of privacy than some democratic governments. This article proposes to view the Apple/Google API in terms of a broader phenomenon whereby tech corporations are encroaching into ever new spheres of social life. From this perspective, the advantage these actors have accrued in the sphere of the production of digital goods provides them with access to the spheres of health and medicine, and more worrisome, to the sphere of politics. These sphere transgressions raise numerous risks that are not captured by the focus on privacy harms. Namely, a crowding out of essential spherical expertise, new dependencies on corporate actors for the delivery of essential, public goods, the shaping of public policy by non-representative, private actors and ultimately, the accumulation of decision-making power across multiple spheres. While privacy is certainly an important value, its centrality in the debate on digital contact tracing may blind us to these broader societal harms and unwittingly pave the way for ever more sphere transgressions. (shrink)

Every Berman’s variety \ which is the subvariety of Ockham algebras defined by the equation \ and \) determines a finitary substitution invariant consequence relation \. A sequent system \ is introduced as an axiomatization of the consequence relation \. The system \ is characterized by a single finite frame \ under the frame semantics given for the formal language. By the duality between frames and algebras, \ can be viewed as a \-valued logic as it is characterized by (...) a distributive lattice of \ elements with a unary operator. Moreover, a structural-rule-free, cut-free and terminating sequent system \ is established for \. The Craig interpolation property of \ is shown proof-theoretically utilizing \. (shrink)

In this paper, we have developed an Excel package to be utilized for calculating neutrosophic data and analyze them. The use of object oriented programming techniques and concepts as they may apply to the design and development a new framework to implement neutrosophic data operations, the c# programming language, NET Framework and Microsoft Visual Studio are used to implement the neutrosophic classes. We have used Excel as it is a powerful tool that is widely accepted and used for statistical analysis. (...) Figure 1 shows Class Diagram of the implemented package. Figure 2 presents a working example of the package interface calculating the complement. Our implemented Neutrosophic package can calculate Intersection, Union, and Complement of the nuetrosophic set. Figure 3 presents our neutrosphic package capability to draw figures of presented neutrosphic set. Figure 4 presents charting of Union operation calculation, and figure 5 Intersection Operation. nuetrosophic set are characterized by its efficiency as it takes into consideration the three data items: True, Intermediate, and False. (shrink)

Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in (...) the context of nested sequents, referred to as "coloring," which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These "certificates" (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input. (shrink)

The "Dark Side" of Humour. An Analysis of Subversive Humour in Workplace Emails Although a substantial amount of research has investigated the various functions of humour in a workplace context, electronic means of communication have largely been ignored. This is particularly surprising since electronic communication in the workplace is increasingly gaining significance. This seems to be especially true for email, which in many workplaces is the preferred medium for communicating transactional as well as relational topics. Drawing on a corpus (...) of about 100 emails collected in an academic setting, we explore how humour is used in workplace emails. Our specific focus is on subversive humour, which often functions as a tool to express frustration and dissent, and ultimately to challenge existing power relations. Our analysis illustrates that subversive humour is an excellent means to make fun of established and normative workplace practices by exaggerating and ridiculing them, and to re-define organisational reality by offering alternative interpretations. These functions of subversive humour appear to be particularly useful for those in relatively powerful positions: by employing humour to convey critical and potentially threatening messages in acceptable ways, the senders manage to express their dissent and frustration with the wider organisational system while, at the same time, escaping the scrutiny of the very organisation that they are symbolically challenging. (shrink)

ABSTRACT Diana Mutz's individual-level data show that participation and deliberation are often inversely related. This, according to Mutz, undermines many claims made by deliberative-democratic theory. However, a systemic approach to deliberative democracy challenges the significance of this finding. Although it is true that some citizens are political activists not open to hearing the other side and other citizens are less active but more open minded, both types of citizens make equally important and positive contributions to deliberative politics when it (...) is viewed as a system that deploys a division of labor. (shrink)

In this paper, we have developed an Excel package to be utilized for calculating neutrosophic data and analyze them. The use of object oriented programming techniques and concepts as they may apply to the design and development a new framework to implement neutrosophic data operations, the c# programming language, NET Framework and Microsoft Visual Studio are used to implement the neutrosophic classes. We have used Excel as it is a powerful tool that is widely accepted and used for statistical analysis. (...) Figure 1 shows Class Diagram of the implemented package. Figure 2 presents a working example of the package interface calculating the complement. Our implemented Neutrosophic package can calculate Intersection, Union, and Complement of the neutrosophic set. Figure 3 presents our neutrosophic package capability to draw figures of presented neutrosophic set. Figure 4 presents charting of Union operation calculation, and figure 5 Intersection Operation. neutrosophic set are characterized by its efficiency as it takes into consideration the three data items: True, Intermediate, and False. -/- . (shrink)

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version (...) of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form. (shrink)

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, (...) weakening and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure. (shrink)

We can readily identify goal-directed systems and distinguish them from non-goal-directed systems. A woodpecker hunting for grubs is the first, a pendulum returning to rest is the second. But what is it to be a goal-directed system? Perhaps the dominant answer to this question, inspired by systems theories such as cybernetics, is that goal-directed systems are distinguished by their tendency to seek, aim at, or maintain some more-or-less easily identifiable goal. Cybernetics and the like would hold (...) that physical systems subject only to physical laws can exhibit such behavior. If sound, this systems approach to teleology would unify a diverse range of goal-directed phenomena and neatly side-step many traditional bogey-men of teleology, such as anthropomorphism and future causation. Goal-directed phenomena would be a normal feature of the natural causal world that could be described in purely descriptive and quantitative terms, and receive ordinary causal explanations. Thus, the systems approach promises to provide a naturalistic-cum-descriptive account of teleology suitable for use in naturalistic accounts of other phenomena, including the intentionality of mental states and even self-consciousness. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: (...) all changes are made in the structural rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Barbarous On Either Side: The New York Blues Of Mr. Sammler’s PlanetStanley CrouchThere are no two ways about virtue, my dear student; it either is, or it is not. Talk of doing penance for your sins! It is a nice system of business, when you pay for your crime by an act of contrition! You seduce a woman that you may set your foot on such and such a (...) rung of the social ladder; you sow dissension among the children of a family; you descend, in short, to every base action that can be committed at home or abroad, to gain your own ends for you own pleasure or profit.... That man with yellow gloves and a golden tongue commits many a murder; he sheds no blood, but he drains his victims as surely; a desperado forces open a door with a crowbar, dark deeds both of them! You yourself will do every one of the things that I suggested to you today, bar the bloodshed. Do you believe there is any absolute standard in this world?—Vautrin, Père GoriotWe are now mightily perplexed by the vulgarity and the brutal appetites of our culture, which Mr. Sammler sees so, so clearly, startled from page to page and in passage after passage of Saul Bellow’s 1970 novel. The terrible children of our day, the worst of our politicians, and the rampant sleaze that slides up and down the classes, across the races and religions, from the cynical students to the unrepentingly jaded and old, can be traced back to the elements that are so alarming to the protagonist of Mr. Sammler’s Planet. As a well-educated man who has smelled the molten breath and felt the bloody teeth of European fascism, Mr. Sammler is obsessed with understanding what makes or breaks a society, what causes a civilization to embrace ruthlessness as the [End Page 89] best way to realize its ambitions and handle its fears. A veteran of World War II, he has seen killing and he has done it himself, which makes him a man for whom none of his questions exists in a speculative air unfouled by the odor of murder. His intellectual ponderings are thereby part of a drama in which he has seen the lowest the Western world has to offer. This lack of innocence makes him a hero and a thinker haunted by his past and startled to uneasiness by the present. Oh, yes: Artur Sammler knows firsthand how quickly the metamorphosis from the refined to the smugly savage can take place. “Like many people who had seen the world collapse once, Mr. Sammler entertained the possibility it might collapse twice.”The very conception of Mr. Sammler is expressive of Bellow’s gift for bringing together the intellect, the passion, the spirit, and the flesh. The physical responses to stimulation are rendered with the same attention given to all of the many things that Mr. Sammler contemplates as he tries to get a grip on New York, America’s financial capital and the pinnacle of the nation’s culture. Mr. Sammler’s ideas are counterpointed by feeling and sensuality to such a degree that the thoughts are themselves elements of emotion, which is something only our finest writers can bring off, the literary condition of character so complete that every aspect of consciousness takes form within the container of a body equal in the life of its senses to the spirit it carries. We get the feeling of a human being in repose, in grief, in rage, in self-protective contemplation, in unsparing self-examination, in attentive motion through Manhattan, on foot, in public transportation, in chauffeured limousine.New York’s power over the country was central to why it was chosen as the place of action. Mr. Sammler could not be in a better setting if he were to wrestle with the identity of the United States. One part of it obviously has to do with the character’s Jewishness. Manhattan and Hollywood are the two places where Jews have made their deepest imprints on the country. Unlike the dream factory of Hollywood, New York is the city... (shrink)

Compact Bilinear Logic , introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut-elimination theorem for them. We also discuss a connection between cut-elimination for CBL and the Switching Lemma from [14].

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with (...) only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\). (shrink)

In this paper, we study multiplicative extensions of propositional many-place sequent calculi for finitely-valued logics arising from those introduced in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) through their translation by means of singularity determinants for logics and restriction of the original many-place sequent language. Our generalized approach, first of all, covers, on a uniform formal basis, both the one developed in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) (...) for singular finitely-valued logics (when singularity determinants consist of a variable alone) and conventional Gentzen-style (i.e., two-place sequent) calculi suggested in Pynko (Bull Sect Logic 33(1):23–32, 2004) for finitely-valued logics with equality determinant. In addition, it provides a universal method of constructing Tait-style (i.e., one-place sequent) calculi for finitely-valued logics with singularity determinant (in particular, for Łukasiewicz finitely-valued logics) that fits the well-known Tait calculus (Lecture Notes in Mathematics, Springer, Berlin, 1968) for the classical logic. We properly extend main results of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) and explore calculi under consideration within the framework of Sect. 7 of Pynko (Arch Math Logic 45:267–305, 2006), generalizing the results obtained in Sect. 7.5 of Pynko (Arch Math Logic 45:267–305 2006) for two-place sequent calculi associated with finitely-valued logics with equality determinant according to Pynko (Bull Sect Logic 33(1):23–32, 2004). We also exemplify our universal elaboration by applying it to some denumerable families of well-known finitely-valued logics. (shrink)

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out (...) this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of prepositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related to BCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never (...) changed: all changes are made in the structural rules. Next, Hilbert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.Below is the sequel to the first part of the paper, which appeared in the previous issue of this journal (vol. 47 (1988), pp. 353–386). The first part contained sections on sequent-systems and Hilbert-formulations, and here is the third section on groupoid models. This second part is meant to be read in conjunction with the first part. (shrink)

Autonomous weapons systems (AWS), sometimes referred to as “killer robots”, are receiving evermore attention, both in public discourse as well as by scholars and policymakers. Much of this interest is connected with emerging ethical and legal problems linked to increasing autonomy in weapons systems, but there is a general underappreciation for the ways in which existing law might impact on these new technologies. In this paper, we argue that as AWS become more sophisticated and increasingly more capable than (...) flesh-and-blood soldiers, it will increasingly be the case that such soldiers are “in the power” of those AWS which fight against them. This implies that such soldiers ought to be considered hors de combat, and not targeted. In arguing for this point, we draw out a broader conclusion regarding hors de combat status, namely that it must be viewed contextually, with close reference to the capabilities of combatants on both sides of any discreet engagement. Given this point, and the fact that AWS may come in many shapes and sizes, and can be made for many different missions, we argue that each particular AWS will likely need its own standard for when enemy soldiers are deemed hors de combat. We conclude by examining how these nuanced views of hors de combat status might impact on meaningful human control of AWS. (shrink)

During periods of scarcity, or the fear of it, many health systems create or adopt triage protocols to determine how to best allocate limited resources. Interest in such protocols has become acute...

This article introduces, studies, and applies a new system of logic which is called ‘HYPE’. In HYPE, formulas are evaluated at states that may exhibit truth value gaps and truth value gluts. Simple and natural semantic rules for negation and the conditional operator are formulated based on an incompatibility relation and a partial fusion operation on states. The semantics is worked out in formal and philosophical detail, and a sound and complete axiomatization is provided both for the propositional and the (...) predicate logic of the system. The propositional logic of HYPE is shown to contain first-degree entailment, to have the Finite Model Property, to be decidable, to have the Disjunction Property, and to extend intuitionistic propositional logic conservatively when intuitionistic negation is defined appropriately by HYPE’s logical connectives. Furthermore, HYPE’s first-order logic is a conservative extension of intuitionistic logic with the Constant Domain Axiom, when intuitionistic negation is again defined appropriately. The system allows for simple model constructions and intuitive Euler-Venn-like diagrams, and its logical structure matches structures well-known from ordinary mathematics, such as from optimization theory, combinatorics, and graph theory. HYPE may also be used as a general logical framework in which different systems of logic can be studied, compared, and combined. In particular, HYPE is found to relate in interesting ways to classical logic and various systems of relevance and paraconsistent logic, many-valued logic, and truthmaker semantics. On the philosophical side, if used as a logic for theories of type-free truth, HYPE is shown to address semantic paradoxes such as the Liar Paradox by extending non-classical fixed-point interpretations of truth by a conditional as well-behaved as that of intuitionistic logic. Finally, HYPE may be used as a background system for modal operators that create hyperintensional contexts, though the details of this application need to be left to follow-up work. (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)

For centuries, the trickster has been used in various narratives, including mythological, literary and cinematic, to convey the idea of agency, rebellion and, often turbulent, progress. In _The Trickster and the System: Identity and Agency in Contemporary Society_,_ __Helena Bassil-Morozow_ shows how the trickster can be seen as a metaphor to describe the psycho-anthropological concept of change, an impulse that challenges the existing order of things, a progressive force that is a-structural and anti-structural in its nature. The book is about (...) being able to see things from an unusual, even ‘odd’, perspective, which does not coincide with the homogenous normality of the mass, or the social system, or a political ideology, or some other kind of authority. The Trickster and the System offers an analytical paradigm which can be used to examine relationships between tricksters and systems, change and stability, in a wide range of social, political and cultural contexts. It covers a range of systems, describes different types of tricksters and discusses possible conflicts, tensions and dialogues between the two opposing sides. One of the central ideas of the book is that social systems use shame as a tool to control and manage all kinds of tricksters – individuality, agency, creativity, spontaneity, innovation and initiative, to name but a few. The author argues that any society that neglects its tricksters, ends up suffering from decay, stagnation – or even mass hysterical outbursts. The Trickster and the System: Identity and Agency in Contemporary Society provides a fresh perspective on the trickster figure in a variety of cultural contexts. It covers a range of psychological, cultural, social and political phenomena, from personal issues to the highest level of society’s functioning: self-esteem and shame, lifestyle and relationships, creativity and self-expression, media, advertising, economy, political ideology and, most importantly, human identity and authenticity. The book is essential reading for scholars in the areas of psychoanalysis, analytical psychology, myth, cultural and media studies, narrative analysis, cultural anthropology, as well as anyone interested in critical issues in contemporary culture. Helena Bassil-Morozow is a cultural philosopher, film scholar and academic writer whose many publications include _Tim Burton: The Monster and the Crowd _ and _The Trickster in Contemporary Film _. Helena is currently working on another Routledge project, _Jungian Film Studies: the Essential Guide _. Her principal academic affiliation is the University of Bedfordshire, Faculty of Creative Arts, Technologies & Science. (shrink)

Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-classical negations that live inside very natural systems of normal modal logics over complete distributive lattices; these logics are further enriched by adjustment connectives that may (...) be used for handling reasoning under uncertainty caused by inconsistency or undeterminedness. Using such straightforward semantics, we study the classes of frames characterized by seriality, reflexivity, functionality, symmetry, transitivity, and some combinations thereof, and discuss what they reveal about sub-classical properties of negation. To the logics thereby characterized we apply a general mechanism that allows one to endow them with analytic ordinary sequent systems, most of which are even cut-free. We also investigate the exact circumstances that allow for classical negation to be explicitly defined inside our logics. (shrink)

The Polish logician Roman Suszko has extensively pleaded in the 1970s for a restatement of the notion of many-valuedness. According to him, as he would often repeat, “there are but two logical values, true and false.” As a matter of fact, a result by W´ojcicki-Lindenbaum shows that any tarskian logic has a many-valued semantics, and results by Suszko-da Costa-Scott show that any many-valued semantics can be reduced to a two-valued one. So, why should one even consider using (...) logics with more than two values? Because, we argue, one has to decide how to deal with bivalence and settle down the tradeoff between logical 2-valuedness and truth-functionality, from a pragmatical standpoint. -/- This paper will illustrate the ups and downs of a two-valued reduction of logic. Suszko’s reductive result is quite non-constructive.We will exhibit here a way of effectively constructing the two-valued semantics of any logic that has a truth-functional finite-valued semantics and a sufficiently expressive language. From there, as we will indicate, one can easily go on to provide those logics with adequate canonical systems of sequents or tableaux. The algorithmic methods developed here can be generalized so as to apply to many non-finitely valued logics as well —or at least to those that admit of computable quasi tabular two-valued semantics, the so-called dyadic semantics. (shrink)

We present a number of equivalent calculi for many-valued logics and prove soundness and strong completeness theorems. The calculi are obtained from the truth tables of the logic under consideration in a straightforward manner and there is a natural duality among these calculi. We also prove the cut elimination theorems for the sequent-like systems.

The deep and many-sided penetration of mathematical methods into virtually all branches of scientific knowledge is a characteristic feature of the present period of development of human culture. Even fields so remote from mathematics as the theory of versification, jurisprudence, archeology, and medical diagnostics have now proved to be associated with the accelerating process of application of disciplines such as probability theory, information theory, algorithm theory, etc. Mathematical methods are rapidly penetrating the sphere of the social sciences. One (...) can no longer speak of the "exact" sciences in the traditional sense , for today they cannot even be conceived of without the most powerful mathematical "armament." These highly complex processes proceed differently, of course, in different sciences. Let us attempt to analyze them, with our chief emphasis upon the experience of the progress of astronomy, mechanics, physics, and other "exact" branches of natural science. (shrink)