The present paper wants to promote epistemic pluralism as an alternative view of non-classical logics. For this purpose, a bilateralist logic of acceptance and rejection is developed in order to make an important di erence between several concepts of epistemology, including information and justi cation. Moreover, the notion of disagreement corresponds to a set of epistemic oppositions between agents. The result is a non-standard theory of opposition for many-valued logics, rendering total and partial disagreement in terms of epistemic negation and (...) semi-negations. (shrink)

This paper reviews the central points and presents some recent developments of the epistemic approach to paraconsistency in terms of the preservation of evidence. Two formal systems are surveyed, the basic logic of evidence (BLE) and the logic of evidence and truth (LET J ), designed to deal, respectively, with evidence and with evidence and truth. While BLE is equivalent to Nelson’s logic N4, it has been conceived for a different purpose. Adequate valuation semantics that provide decidability are given for (...) both BLE and LET J . The meanings of the connectives of BLE and LET J , from the point of view of preservation of evidence, is explained with the aid of an inferential semantics. A formalization of the notion of evidence for BLE as proposed by M. Fitting is also reviewed here. As a novel result, the paper shows that LET J is semantically characterized through the so-called Fidel structures. Some opportunities for further research are also discussed. (shrink)

Argumentation is a form of reasoning where a claim is accepted or rejected according to the analysis of the arguments for and against it; furthermore, it provides a reasoning mechanism able to handle contradictory, incomplete and uncertain information in real-world situations. We combine Bipolar Argumentation Frameworks (an extension of Dung’s work) with an Algebra of Argumentation Labels modeling two independent types of interaction between arguments, representing meta-information associated with arguments, and introducing an acceptability notion that will give more information for (...) arguments acceptability. (shrink)

We introduce and study a new approach to the theory of abstract algebraic logic (AAL) that explores the use of many-sorted behavioral logic in the role traditionally played by unsorted equational logic. Our aim is to extend the range of applicability of AAL toward providing a meaningful algebraic counterpart also to logics with a many-sorted language, and possibly including non-truth-functional connectives. The proposed behavioral approach covers logics which are not algebraizable according to the standard approach, while also bringing a new (...) algebraic perspective to logics which are algebraizable using the standard tools of AAL. Furthermore, we pave the way toward a robust behavioral theory of AAL, namely by providing a behavioral version of the Leibniz operator which allows us to generalize the traditional Leibniz hierarchy, as well as several well-known characterization results. A number of meaningful examples will be used to illustrate the novelties and advantages of the approach. (shrink)

We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly clarify the relationships of our falsification logic to (...) some other logical systems. (shrink)

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. (shrink)

This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we do not want to (...) equate falsity with the non-existence of a proof since this would render a statement such as “pi is transcendental” false prior to 1882. In addition, the intuitionist account of negation as shorthand for the derivation of absurdity is inadequate, particularly outside of purely mathematical contexts. To deal with these issues, I investigate the dual of intuitionistic logic, co-intuitionistic logic, as a logic of refutation, alongside intuitionistic logic of proofs. Direct proof and refutation are dual to each other, and are constructive, whilst there also exist syntactic, weak, negations within both logics. In this respect, the logic of refutation is weakly paraconsistent in the sense that it allows for statements for which, neither they, nor their negation, are refuted. I provide a proof theory for the co-constructive logic, a formal dualizing map between the logics, and a Kripke-style semantics. This is given an intuitive philosophical rendering in a re-interpretation of Kolmogorov’s logic of problems. (shrink)

We examine the relationship between the logics of nonsense of Bochvar and Halldén and the containment logics in the neighborhood of William Parry’s A I. We detail two strategies for manufacturing containment logics from nonsense logics—taking either connexive and paraconsistent fragments of such systems—and show how systems determined by these techniques have appeared as Frederick Johnson’s R C and Carlos Oller’s A L. In particular, we prove that Johnson’s system is precisely the intersection of Bochvar’s B 3 and Graham Priest’s (...) non-symmetrized connexive logic and that Oller’s system lies just beneath the intersection of B 3 and Priest’s paraconsistent L P. We conclude by examining Oller’s system in more depth, giving it a characterization in terms of L P and showing that it plays the same role to Harry Deutsch’s paraconsistent containment logic S that Aleksandr Zinov'ev’s S 1 plays with respect to A I. (shrink)

A B S T R AC T: In this paper I consider an interpretation of future contingents which motivates a unification of a Łukasiewicz-style logic with the more classical supervaluational semantics. This in turn motivates a new non-classical logic modelling what is “made true by history up until now. ” I give a simple Hilbert-style proof theory, and a soundness and completeness argument for the proof theory with respect to the intended models.

In this paper, a family of paraconsistent propositional logics with constructive negation, constructive implication, and constructive co-implication is introduced. Although some fragments of these logics are known from the literature and although these logics emerge quite naturally, it seems that none of them has been considered so far. A relational possible worlds semantics as well as sound and complete display sequent calculi for the logics under consideration are presented.

There are several three-valued logical systems that form a scattered landscape, even if all reasonable connectives in three-valued logics can be derived from a few of them. Most papers on this subject neglect the issue of the relevance of such logics in relation with the intended meaning of the third truth-value. Here, we focus on the case where the third truth-value means unknown, as suggested by Kleene. Under such an understanding, we show that any truth-qualified formula in a large range (...) of three-valued logics can be translated into KD as a modal formula of depth 1, with modalities in front of literals only, while preserving all tautologies and inference rules of the original three-valued logic. This simple information logic is a two-tiered classical propositional logic with simple semantics in terms of epistemic states understood as subsets of classical interpretations. We study in particular the translations of Kleene, Gödel, ᴌukasiewicz and Nelson logics. We show that Priest’s logic of paradox, closely connected to Kleene’s, can also be translated into our modal setting, simply by exchanging the modalities possible and necessary. Our work enables the precise expressive power of three-valued logics to be laid bare for the purpose of uncertainty management. (shrink)

In a previous work we studied, from the perspective ofAlgebraic Logic, the implicationless fragment of a logic introduced by O. Arieli and A. Avron using a class of bilattice-based logical matrices called logical bilattices. Here we complete this study by considering the Arieli-Avron logic in the full language, obtained by adding two implication connectives to the standard bilattice language. We prove that this logic is algebraizable and investigate its algebraic models, which turn out to be distributive bilattices with additional implication (...) operations. We axiomatize and state several results on these new classes of algebras, in particular representation theorems analogue to the well-known one for interlaced bilattices. (shrink)

In this paper, we look at applying the techniques from analyzing superintuitionistic logics to extensions of the cointuitionistic Priest-da Costa logic daC (introduced by Graham Priest as “da Costa logic”). The relationship between the superintuitionistic axioms- definable in daC- and extensions of Priest-da Costa logic (sdc-logics) is analyzed and applied to exploring the gap between the maximal si-logic SmL and classical logic in the class of sdc-logics. A sequence of strengthenings of Priest-da Costa logic is examined and employed to pinpoint (...) the maximal non-classical extension of both daC and Heyting-Brouwer logic HB . Finally, the relationship between daC and Logics of Formal Inconsistency is examined. (shrink)

In this paper, we give an algebraic completeness theorem for constructive logic with strong negation in terms of finite rough set-based Nelson algebras determined by quasiorders. We show how for a quasiorder R, its rough set-based Nelson algebra can be obtained by applying Sendlewski’s well-known construction. We prove that if the set of all R-closed elements, which may be viewed as the set of completely defined objects, is cofinal, then the rough set-based Nelson algebra determined by the quasiorder R forms (...) an effective lattice, that is, an algebraic model of the logic E 0, which is characterised by a modal operator grasping the notion of “to be classically valid”. We present a necessary and sufficient condition under which a Nelson algebra is isomorphic to a rough set-based effective lattice determined by a quasiorder. (shrink)

In this paper, we define a first-order logic CFʹ with strong negation and bounded static quantifiers, which is a variant of Thomason's logic CF. For the logic CFʹ, the usual Kripke formal semantics is defined based on situations, and a sound and complete axiomatic system is established based on the axiomatic systems of constructive logics with strong negation and Thomason's completeness proof techniques. With the use of bounded quantifiers, CFʹ allows the domain of quantification to be empty and allows for (...) nondenoting constants. CFʹ is intended as a fragment of a logic for situation theory. Thus the connection between CFʹ and infon logic is discussed. (shrink)

According to one tradition in realist philosophy, 'truthmaking' amounts to necessitation. That is, an object x is a truthmaker for the claim A if x exists, and the existence of x necessitates the truth of A. I argued in my paper "Truthmakers, Entailment and Necessity" [14], that if we wish to use this account of truthmaking, we ought understand the entailment connective "=>" in such a claim as a relevant entailment, in the tradition of Anderson and Belnap and their co-workers (...) [1, 2, 8, 11]. Furthermore, I proposed a number of theses about truthmaking as necessitation. The most controversial of these is the disjunction thesis: x makes a disjunction A v B true if and only if it makes one of the disjuncts (A or B) true. That paper left one important task unfinished. I did not explain how the theses about truthmaking could be true together. In this paper I give a consistency proof, by providing a model for the theses of truthmaking in my earlier paper. This result does two things. First, it shows that the theses of truthmaking are jointly consistent. Second, it provides an independently philosophically motivated formal model for relevant logics in the 'possible worlds' tradition of Routley and Meyer [8, 16, 17]. (shrink)

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.

A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.

This paper deals with, prepositional calculi with strong negation (N-logics) in which the Craig interpolation theorem holds. N-logics are defined to be axiomatic strengthenings of the intuitionistic calculus enriched with a unary connective called strong negation. There exists continuum of N-logics, but the Craig interpolation theorem holds only in 14 of them.

Consequence is at the heart of logic; an account of consequence, of what follows from what, offers a vital tool in the evaluation of arguments. Since philosophy itself proceeds by way of argument and inference, a clear view of what logical consequence amounts to is of central importance to the whole discipline. In this book JC Beall and Greg Restall present and defend what thay call logical pluralism, the view that there is more than one genuine deductive consequence relation, a (...) position which has profound implications for many linguists as well as for philosophers. We should not search for one true logic, since there are many. (shrink)

The paper extends a framework of information-based semantics for intuitionistic logic with a paraconsistent negation and consistency-sensitive epistemic modalities. In this framework information states represent information collected from various sources and as such they can be inconsistent because they receive contradictory information either from a single inconsistent source or from various mutually incompatible sources. The modalities reflect only those sources that are consistent and trusted. For the paraconsistent logic generated by this framework, we present a Hilbert style system, we prove (...) completeness, the disjunction property, the finite model property and various other results. (shrink)

In this paper, we use the concept of very true operator to pre-semi-Nelson algebras and investigate the properties of very true pre-semi-Nelson algebras. We study the very true N-deductive systems and use them to establish the uniform structure on very true pre-semi-Nelson algebras. We obtain some properties of this topology. Finally, the corresponding logic very true semi-intuitionistic logic with strong negation is constructed and algebraizable of this logic is proved based on very true semi-Nelson algebras.

Over the past 50 years, Nelson algebras have been extensively studied by distinguished scholars as the algebraic counterpart of Nelson's constructive logic with strong negation. Despite these studies, a comprehensive survey of the topic is currently lacking, and the theory of Nelson algebras remains largely unknown to most logicians. This paper aims to fill this gap by focussing on the essential developments in the field over the past two decades. Additionally, we explore generalisations of Nelson algebras, such as N4-lattices which (...) correspond to the paraconsistent version of Nelson's logic, as well as their applications to other areas of interest to logicians, such as duality and rough set theory. A general representation theorem states that each Nelson algebra is isomorphic to a subalgebra of a rough set-based Nelson algebra induced by a quasiorder. Furthermore, a formula is a theorem of Nelson logic if and only if it is valid in every finite Nelson algebra induced by a quasiorder. (shrink)

Two new propositional non-classical logics, referred to as symmetric intuitionistic logic (SIL) and conflated intuitionistic logic (CIL), are introduced as indexed and non-indexed Gentzen-style sequent calculi. SIL is regarded as a natural hybrid logic combining intuitionistic and dual-intuitionistic logics, whereas CIL is regarded as a variant of intuitionistic paraconsistent logic with conflation and without paraconsistent negation. The cut-elimination theorems for SIL and CIL are proved. CIL is shown to be conservative over SIL.

Recent research on algebraic models of _quasi-Nelson logic_ has brought new attention to a number of classes of algebras which result from enriching (subreducts of) Heyting algebras with a special modal operator, known in the literature as a _nucleus_. Among these various algebraic structures, for which we employ the umbrella term _intuitionistic modal algebras_, some have been studied since at least the 1970s, usually within the framework of topology and sheaf theory. Others may seem more exotic, for their primitive operations (...) arise from algebraic terms of the intuitionistic modal language which have not been previously considered. We shall for instance investigate the variety of _weak implicative semilattices_, whose members are (non-necessarily distributive) meet semilattices endowed with a nucleus and an implication operation which is not a relative pseudo-complement but satisfies the postulates of Celani and Jansana’s strict implication. For each of these new classes of algebras we establish a representation and a topological duality which generalize the known ones for Heyting algebras enriched with a nucleus. (shrink)

Although the work of G.F.C. Griss is commonly understood as a program of negationless mathematics, close examination of Griss’s work suggests a more fundamental feature is its executability, a requirement that mental constructions are possible only if corresponding mental activity can be actively carried out. Emphasizing executability reveals that Griss’s arguments against negation leave open several types of negation—including D. Nelson’s strong negation—as compatible with Griss’s intuitionism. Reinterpreting Griss’s program as one of executable mathematics, we iteratively develop a pair of (...) bilateral constructive logics and argue for their adequacy as accounts of the propositional basis of Griss’s work. We conclude by observing connexive features exhibited by the two bilateral logics and by investigating the difficulties connexive principles reveal for the development of executable mathematics. (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)

Quasi-Nelson logic (QNL) was recently introduced as a common generalisation of intuitionistic logic and Nelson's constructive logic with strong negation. Viewed as a substructural logic, QNL is the axiomatic extension of the Full Lambek Calculus with Exchange and Weakening by the Nelson axiom, and its algebraic counterpart is a variety of residuated lattices called quasi-Nelson algebras. Nelson's logic, in turn, may be obtained as the axiomatic extension of QNL by the double negation (or involutivity) axiom, and intuitionistic logic as the (...) extension of QNL by the contraction axiom. A recent series of papers by the author and collaborators initiated the study of fragments of QNL, which correspond to subreducts of quasi-Nelson algebras. In the present paper we focus on fragments that contain the connectives forming a residuated pair (the monoid conjunction and the so-called strong Nelson implication), these being the most interesting ones from a substructural logic perspective. We provide quasi-equational (whenever possible, equational) axiomatisations for the corresponding classes of algebras, obtain twist representations for them, study their congruence properties and take a look at a few notable subvarieties. Our results specialise to the involutive case, yielding characterisations of the corresponding fragments of Nelson's logic and their algebraic counterparts. (shrink)

The mathematician G.F.C. Griss is known for his program of negationless intuitionistic mathematics. Although Griss’s rejection of negation is regarded as characteristic of his philosophy, this is a consequence of an executability requirement that mental constructions presuppose agents’ executing corresponding mental activity. Restoring Griss’s executability requirement to a central role permits a more subtle characterization of the rejection of negation, according to which D. Nelson’s strong constructible negation is compatible with Griss’s principles. This exposes a ‘holographic’ theory of negation in (...) negationless mathematics, in which a full theory of negation is ‘flattened’ in a putatively negationless setting. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

Il s’agit de comprendre dans cet article l’opposition formulée par Gilles-Gaston Granger entre deux types de négation : la négation « radicale », d’un côté, et les négations « appliquées » de l’autre. Nous examinerons les propriétés de cette opposition, ainsi que les enseignements à en tirer sur la philosophie de la logique de Granger. Puis nous proposerons une théorie constructive des valeurs logiques considérées comme des objets structurés, consolidant à la fois l’unité de la théorie logique de Granger et (...) son pluralisme philosophique. (shrink)

Besides the better-known Nelson logic and paraconsistent Nelson logic, in 1959 David Nelson introduced, with motivations of realizability and constructibility, a logic called $\mathcal{S}$. The logic $\mathcal{S}$ was originally presented by means of a calculus with infinitely many rule schemata and no semantics. We look here at the propositional fragment of $\mathcal{S}$, showing that it is algebraizable, in the sense of Blok and Pigozzi, with respect to a variety of three-potent involutive residuated lattices. We thus introduce the first known algebraic (...) semantics for $\mathcal{S}$ as well as a finite Hilbert-style calculus equivalent to Nelson’s presentation; this also allows us to clarify the relation between $\mathcal{S}$ and the other two Nelson logics $\mathcal{N}3$ and $\mathcal{N}4$. (shrink)

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)

In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...) determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

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 CLScw (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 CLScw, 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. (shrink)

David Nelson’s constructive logics with strong negation may beviewed as alternative paraconsistent logic. These logics have been developedbefore da Costa’s works. We address some philosophical aspects of Nelson’slogics and give technical results concerning Kripke models and tableau calculi. We also suggest possible applications of paraconsistent constructivelogics.

ABSTRACT In the paper we present a survey of some approaches to the semantics of many-valued propositional systems. These approaches are inspired on one hand by classical problems in the investigations of logical aspects of epistemic activity: knowledge and truth, contradictions, beliefs, reliability of data, etc. On the other hand they reflect contemporary concerns of researchers in Artificial Intelligence (and Cognitive Science in general) with inferences drawn from imperfect information, even from total ignorance. We treat the mathematical apparatus that has (...) emerged recently: algebraic structures related to the new logical systems in the same way Boolean algebras correspond to classical logic. (shrink)

The motivation for Core Logic is explained. Its system of proof is set out. It is then shown that, although the system has no Cut rule, its relation of deducibility obeys Cut with epistemic gain.

The trilattice SIXTEEN3 introduced in Shramko & Wansing (2005) is a natural generalization of the famous bilattice FOUR2. Some Hilbert-style proof systems for trilattice logics related to SIXTEEN3 have recently been studied (Odintsov, 2009; Shramko & Wansing, 2005). In this paper, three sequent calculi GB, FB, and QB are presented for Odintsovs coordinate valuations associated with valuations in SIXTEEN3. The equivalence between GB, FB, and QB, the cut-elimination theorems for these calculi, and the decidability of B are proved. In addition, (...) it is shown how the sequent systems for B can be extended to cut-free sequent calculi for Odintsov’s LB, which is an extension of B by adding classical implication and negation connectives. (shrink)