Gentzen-Type Methods for Bilattice Negation

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLS_cw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLS_cw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL.     

Rough Sets and 3-Valued Logics

In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics. We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness” operator.     

Nelson's Negation on the Base of Weaker Versions of Intuitionistic Negation

Constructive logic with Nelson negation is an extension of the intuitionistic logic with a special type of negation expressing some features of constructive falsity and refutation by counterexample. In this paper we generalize this logic weakening maximally the underlying intuitionistic negation. The resulting system, called subminimal logic with Nelson negation, is studied by means of a kind of algebras called generalized N-lattices. We show that generalized N-lattices admit representation formalizing the intuitive idea of refutation by means of counterexamples giving in this way a counterexample semantics of the logic in question and some of its natural extensions. Among the extensions which are near to the intuitionistic logic are the minimal logic with Nelson negation which is an extension of the Johansson's minimal logic with Nelson negation and its in a sense dual version — the co-minimal logic with Nelson negation. Among the extensions near to the classical logic are the well known 3-valued logic of Lukasiewicz, two 12-valued logics and one 48-valued logic. Standard questions for all these logics — decidability, Kripke-style semantics, complete axiomatizability, conservativeness are studied. At the end of the paper extensions based on a new connective of self-dual conjunction and an analog of the Lukasiewicz middle value ½ have also been considered.     

Counting distinctions: on the conceptual foundations of Shannon’s information theory

Categorical logic has shown that modern logic is essentially the logic of subsets (or “subobjects”). In “subset logic,” predicates are modeled as subsets of a universe and a predicate applies to an individual if the individual is in the subset. Partitions are dual to subsets so there is a dual logic of partitions where a “distinction” [an ordered pair of distinct elements (u, u′) from the universe U] is dual to an “element”. A predicate modeled by a partition π on U would apply to a distinction if the pair of elements was distinguished by the partition π, i.e., if u and u′ were in different blocks of π. Subset logic leads to finite probability theory by taking the (Laplacian) probability as the normalized size of each subset-event of a finite universe. The analogous step in the logic of partitions is to assign to a partition the number of distinctions made by a partition normalized by the total number of ordered |U|² pairs from the finite universe. That yields a notion of “logical entropy” for partitions and a “logical information theory.” The logical theory directly counts the (normalized) number of distinctions in a partition while Shannon’s theory gives the average number of binary partitions needed to make those same distinctions. Thus the logical theory is seen as providing a conceptual underpinning for Shannon’s theory based on the logical notion of “distinctions.” This paper is dedicated to the memory of Gian-Carlo Rota—mathematician, philosopher, mentor, and friend.     

There is More to Negation than Modality

There is a relatively recent trend in treating negation as a modal operator. One such reason is that doing so provides a uniform semantics for the negations of a wide variety of logics and arguably speaks to a longstanding challenge of Quine put to non-classical logics. One might be tempted to draw the conclusion that negation is a modal operator, a claim Francesco Berto (Mind, 124(495), 761–793, 2015) defends at length in a recent paper. According to one such modal account, the negation of a sentence is true at a world x just in case all the worlds at which the sentence is true are incompatible with x. Incompatibility is taken to be the key notion in the account, and what minimal properties a negation has comes down to which minimal conditions incompatibility satisfies. Our aims in this paper are twofold. First, we wish to point out problems for the modal account that make us question its tenability on a fundamental level. Second, in its place we propose an alternative, non-modal, account of negation as a contradictory-forming operator that we argue is superior to, and more natural than, the modal account.     

A Non-deterministic View on Non-classical Negations

We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ⁺, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is based on non-deterministic four-valued or three-valued structures, and prove soundness and completeness for all of them. We show that the role of each rule is to reduce the degree of non-determinism in the corresponding systems. We also show that all the systems considered are decidable, and our semantics can be used for the corresponding decision procedures. Most of the extensions of LJ⁺ (with or without ff) are shown to be conservative over the underlying logic, and it is determined which of them are not.     

Understanding Negation Implicationally in the Relevant Logic R

A star-free relational semantics for relevant logic is presented together with a sound and complete sequent proof theory (display calculus). 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.     

Reductio ad contradictionem: An Algebraic Perspective

We introduce a novel expansion of the four-valued Belnap–Dunn logic by a unary operator representing reductio ad contradictionem and study its algebraic semantics. This expansion thus contains both the direct, non-inferential negation of the Belnap–Dunn logic and an inferential negation akin to the negation of Johansson’s minimal logic. We formulate a sequent calculus for this logic and introduce the variety of reductio algebras as an algebraic semantics for this calculus. We then investigate some basic algebraic properties of this variety, in particular we show that it is locally finite and has EDPC. We identify the subdirectly irreducible algebras in this variety and describe the lattice of varieties of reductio algebras. In particular, we prove that this lattice contains an interval isomorphic to the lattice of classes of finite non-empty graphs with loops closed under surjective graph homomorphisms.     

A First Order Nonmonotonic Extension of Constructive Logic

Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In particular, we prove completeness for .rst-order here-and-there logics, and their minimal strong negation extensions, for both constant and varying domains. We choose the constant domain version, which we denote by QN^c₅, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QN^c₅, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference.     

A base logic for default reasoning

Based on a close study of benchmark examples in default reasoning, such as Nixon Diamond, Penguin Principle, etc., this paper provides an in depth analysis of the basic features of default reasoning. We formalize default inferences based on Modus Ponens for Default Implication, and mark the distinction between “local inferences” (to infer a conclusion from a subset of given premises) and “global inferences” (to infer a conclusion from the entire set of given premises). These conceptual analyses are captured by a formal semantics that is built upon the set-selection function technique. A minimal logic system M of default reasoning that accommodates Modus Ponens for Default Implication and suitable for local inferences is proposed, and its soundness is proved. __________ Translated from Zhexue Yanjiu 哲学研究 (Philosophical Studies), 2003 (special issue) by Ye Feng     

Anderson and Belnap’s Invitation to Sin

Quine has argued that modal logic began with the sin of confusing use and mention. Anderson and Belnap, on the other hand, have offered us a way out through a strategy of nominalization. This paper reviews the history of Lewis’s early work in modal logic, and then proves some results about the system in which “A is necessary” is intepreted as “A is a classical tautology.”     

Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.     

An encompassing framework for Paraconsistent Logic Programs

We propose a framework which extends Antitonic Logic Programs [Damásio and Pereira, in: Proc. 6th Int. Conf. on Logic Programming and Nonmonotonic Reasoning, Springer, 2001, p. 748] to an arbitrary complete bilattice of truth-values, where belief and doubt are explicitly represented. Inspired by Ginsberg and Fitting's bilattice approaches, this framework allows a precise definition of important operators found in logic programming, such as explicit and default negation. In particular, it leads to a natural semantical integration of explicit and default negation through the Coherence Principle [Pereira and Alferes, in: European Conference on Artificial Intelligence, 1992, p. 102], according to which explicit negation entails default negation. We then define Coherent Answer Sets, and the Paraconsistent Well-founded Model semantics, generalizing many paraconsistent semantics for logic programs. In particular, Paraconsistent Well-Founded Semantics with eXplicit negation (WFSX_p) [Alferes et al., J. Automated Reas. 14 (1) (1995) 93–147; Damásio, PhD thesis, 1996]. The framework is an extension of Antitonic Logic Programs for most cases, and is general enough to capture Probabilistic Deductive Databases, Possibilistic Logic Programming, Hybrid Probabilistic Logic Programs, and Fuzzy Logic Programming. Thus, we have a powerful mathematical formalism for dealing simultaneously with default, paraconsistency, and uncertainty reasoning. Results are provided about how our semantical framework deals with inconsistent information and with its propagation by the rules of the program.     

‘Now’ and ‘Then’ in Tense Logic

According to Hans Kamp and Frank Vlach, the two-dimensional tense operators “now” and “then” are ineliminable in quantified tense logic. This is often adduced as an argument against tense logic, and in favor of an extensional account that makes use of explicit quantification over times. The aim of this paper is to defend tense logic against this attack. It shows that “now” and “then” are eliminable in quantified tense logic, provided we endow it with enough quantificational structure. The operators might not be redundant in some other systems of tense logic, but this merely indicates a lack of quantificational resources and does not show any deep-seated inability of tense logic to express claims about time. The paper closes with a brief discussion of the modal analogue of this issue, which concerns the role of the actuality operator in quantified modal logic.     

Constructive Logic with Strong Negation is a Substructural Logic. I

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. This answers a longstanding question of Nelson [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL _ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL _ew . Presented by Heinrich Wansing     

The Rationale Behind Revision-Rule Semantics

According to Gupta and Belnap, the “extensional behavior” of ‘true’ matches that of a circularly defined predicate. Besides promising to explain semantic paradoxicality, their general theory of circular predicates significantly liberalizes the framework of truth-conditional semantics. The authors’ discussions of the rationale behind that liberalization invoke two distinct senses in which a circular predicate’s semantic behavior is explained by a “revision rule” carrying hypothetical information about its extension. Neither attempted explanation succeeds. Their theory may however be modified to employ a relativized notion of extension. The resulting contextualist semantics for ‘true’ construes circularity as a pragmatic phenomenon.     

Constructive Logic with Strong Negation is a Substructural Logic. II

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . The main result of Part I of this series [41] shows that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of deductive systems to establish the definitional equivalence of the logics N and NFL _ew . It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. Presented by Heinrich Wansing     

Truth Values,Neither-true-nor-false,and Supervaluations

The first section (§1) of this essay defends reliance on truth values against those who, on nominalistic grounds, would uniformly substitute a truth predicate. I rehearse some practical, Carnapian advantages of working with truth values in logic. In the second section (§2), after introducing the key idea of auxiliary parameters (§2.1), I look at several cases in which logics involve, as part of their semantics, an extra auxiliary parameter to which truth is relativized, a parameter that caters to special kinds of sentences. In many cases, this facility is said to produce truth values for sentences that on the face of it seem neither true nor false. Often enough, in this situation appeal is made to the method of supervaluations, which operate by “quantifying out” auxiliary parameters, and thereby produce something like a truth value. Logics of this kind exhibit striking differences. I first consider the role that Tarski gives to supervaluation in first order logic (§2.2), and then, after an interlude that asks whether neither-true-nor-false is itself a truth value (§2.3), I consider sentences with non-denoting terms (§2.4), vague sentences (§2.5), ambiguous sentences (§2.6), paradoxical sentences (§2.7), and future-tensed sentences in indeterministic tense logic (§2.8). I conclude my survey with a look at alethic modal logic considered as a cousin (§2.9), and finish with a few sentences of “advice to supervaluationists” (2.10), advice that is largely negative. The case for supervaluations as a road to truth is strong only when the auxiliary parameter that is “quantified out” is in fact irrelevant to the sentences of interest—as in Tarski’s definition of truth for classical logic. In all other cases, the best policy when reporting the results of supervaluation is to use only explicit phrases such as “settled true” or “determinately true,” never dropping the qualification.     

Basic Quasi-Boolean Expansions of Relevance Logics

The basic quasi-Boolean negation (QB-negation) expansions of relevance logics included in Anderson and Belnap’s relevance logic R are defined. We consider two types of QB-negation: H-negation and D-negation. The former one is of paraintuitionistic or superintuitionistic character, the latter one, of dual intuitionistic nature in some sense. Logics endowed with H-negation are paracomplete; logics with D-negation are paraconsistent. All logics defined in the paper are given a Routley-Meyer ternary relational semantics.

     

Everything Else Being Equal: A Modal Logic for <Emphasis Type="Italic">Ceteris Paribus</Emphasis> Preferences

This paper presents a new modal logic for ceteris paribus preferences understood in the sense of “all other things being equal”. This reading goes back to the seminal work of Von Wright in the early 1960’s and has returned in computer science in the 1990’s and in more abstract “dependency logics” today. We show how it differs from ceteris paribus as “all other things being normal”, which is used in contexts with preference defeaters. We provide a semantic analysis and several completeness theorems. We show how our system links up with Von Wright’s work, and how it applies to game-theoretic solution concepts, to agenda setting in investigation, and to preference change. We finally consider its relation with infinitary modal logics.