In this paper we will consider the existing notions of bilateralism in the context of proof-theoretic semantics and propose, based on our understanding of bilateralism, an extension to logical multilateralism. This approach differs from what has been proposed under this name before in that we do not consider multiple speech acts as the core of such a theory but rather multiple consequence relations. We will argue that for this aim the most beneficial proof-theoretical realization is to use sequent calculi with (...) multiple sequent arrows satisfying some specific conditions, which we will lay out in this paper. We will unfold our ideas with the help of a case study in logical tetralateralism and present an extension of Almukdad and Nelson’s propositional constructive four-valued logic by unary operations of meaningfulness and nonsensicality. We will argue that in sequent calculi with multiple sequent arrows it is possible to maintain certain features that are desirable if we assume an understanding of the meaning of connectives in the spirit of proof-theoretic semantics. The use of multiple sequent arrows will be justified by the presence of congruentiality-breaking unary connectives. (shrink)

Despite the tendency to be otherwise, some non-classical logics are known to validate formulas that are invalid in classical logic. A subclass of such systems even possesses pairs of a formula and its negation as theorems, without becoming trivial. How should these provable contradictions be understood? The present paper aims to shed light on aspects of this phenomenon by taking as samples the constructive connexive logic C, which is obtained by a simple modification of a system of constructible falsity, namely (...) N4, as well as its non-constructive extension C3. For these systems, various observations concerning provable contradictions are made, using mainly a proof-theoretic approach. The topics covered in this paper include: how new contradictions are found from parts of provable contradictions; how to characterise provable contradictions in C3 that are constructive; how contradictions can be seen from the relative viewpoint of strong implication; and as an appendix an attempt at generating provable contradictions in C3. (shrink)

In this study, an extended paradefinite logic with classical negation (EPLC), which has the connectives of conflation, paraconsistent negation, classical negation, and classical implication, is introduced as a Gentzen-type sequent calculus. The logic EPLC is regarded as a modification of Arieli, Avron, and Zamansky’s ideal four-valued paradefinite logic (4CC) and as an extension of De and Omori’s extended Belnap–Dunn logic with classical negation (BD+) and Avron’s self-extensional four-valued paradefinite logic (SE4). The completeness, cut-elimination, and decidability theorems for EPLC are proved (...) and EPLC is shown to be embeddable into classical logic. The strong equivalence substitution property and the admissibilities of the rules of negative symmetry, contraposition, and involution are shown for EPLC. Some alternative simple Gentzen-type sequent calculi, which are theorem-equivalent to EPLC, are obtained via these characteristic properties. (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)

A recent paper by Jakl, Jung and Pultr succeeded for the first time in establishing a very natural link between bilattice logic and the duality theory of d-frames and bitopological spaces. In this paper we further exploit, extend and investigate this link from an algebraic and a logical point of view. In particular, we introduce classes of algebras that extend bilattices, d-frames and N4-lattices to a setting in which the negation is not necessarily involutive, and we study corresponding logics. We (...) provide product representation theorems for these algebras, as well as completeness, algebraizability results for the corresponding logics. (shrink)

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int of the bi-intuitionistic (...) logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped. (shrink)

The relationships between various modal logics based on Belnap and Dunn’s paraconsistent four-valued logic FDE are investigated. It is shown that the paraconsistent modal logic \, which lacks a primitive possibility operator \, is definitionally equivalent with the logic \, which has both \ and \ as primitive modalities. Next, a tableau calculus for the paraconsistent modal logic KN4 introduced by L. Goble is defined and used to show that KN4 is definitionally equivalent with \ without the absurdity constant. Moreover, (...) a tableau calculus is defined for the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. It is shown that MBL can be faithfully embedded into the bimodal logic \ over the non-modal vocabulary of MBL. On the way from \ to MBL, the Fischer Servi-style modal logic \ is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE, and \ is shown to be characterized by the class of all models for \. Moreover, \ is axiomatized and this axiom system is proved to be strongly sound and complete with respect to the class of models for \. Moreover, the notion of definitional equivalence is suitably weakened, so as to show that \ and \ are weakly definitionally equivalent. (shrink)

The paper is devoted to the contributions of Helena Rasiowa to the theory of non-classical negation. The main results of Rasiowa in this area concerns–constructive logic with strong (Nelson) negation.

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

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

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.

Dual-intuitionistic logics are logics proposed by Czermak , Goodman and Urbas . It is shown in this paper that there is a correspondence between Goodman's dual-intuitionistic logic and Nelson's constructive logic N−.

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)

The knowability paradox is an instance of a remarkable reasoning pattern (actually, a pair of such patterns), in the course of which an occurrence of the possibility operator, the diamond, disappears. In the present paper, it is pointed out how the unwanted disappearance of the diamond may be escaped. The emphasis is not laid on a discussion of the contentious premise of the knowability paradox, namely that all truths are possibly known, but on how from this assumption the conclusion is (...) derived that all truths are, in fact, known. Nevertheless, the solution offered is in the spirit of the constructivist attitude usually maintained by defenders of the anti-realist premise. In order to avoid the paradoxical reasoning, a paraconsistent constructive relevant modal epistemic logic with strong negation is defined semantically. The system is axiomatized and shown to be complete. (shrink)

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

This paper explores allowing truth value assignments to be undetermined or "partial" and overdetermined or "inconsistent", thus returning to an investigation of the four-valued semantics that I initiated in the sixties. I examine some natural consequence relations and show how they are related to existing logics, including ukasiewicz's three-valued logic, Kleene's three-valued logic, Anderson and Belnap's relevant entailments, Priest's "Logic of Paradox", and the first-degree fragment of the Dunn-McCall system "R-mingle". None of these systems have nested implications, and I investigate (...) twelve natural extensions containing nested implications, all of which can be viewed as coming from natural variations on Kripke's semantics for intuitionistic logic. Many of these logics exist antecedently in the literature, in particular Nelson 's "constructible falsity". (shrink)

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...) subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

We introduce a modal expansion of paraconsistent Nelson logic that is also as a generalization of the Belnapian modal logic recently introduced by Odintsov and Wansing. We prove algebraic completeness theorems for both logics, defining and axiomatizing the corresponding algebraic semantics. We provide a representation for these algebras in terms of twiststructures, generalizing a known result on the representation of the algebraic counterpart of paraconsistent Nelson logic.

Jaśkowski's discussive (discursive) logic D2 is historically one of the first paraconsistent logics, i.e., logics which 'tolerate' contradictions. Following Jaśkowski's idea to define his discussive logic by means of the modal logic S5 via special translation functions between discussive and modal languages, and supporting at the same time the tradition of paracomplete logics being the counterpart of paraconsistent ones, we present a paracomplete discussive logic D2p.

We present a novel treatment of set theory in a four-valued paraconsistent and paracomplete logic, i.e., a logic in which propositions can be both true and false, and neither true nor false. Our approach is a significant departure from previous research in paraconsistent set theory, which has almost exclusively been motivated by a desire to avoid Russell’s paradox and fulfil naive comprehension. Instead, we prioritise setting up a system with a clear ontology of non-classical sets, which can be used to (...) reason informally about incomplete and inconsistent phenomena, and is sufficiently similar to ${\mathrm {ZFC}}$ to enable the development of interesting mathematics. We propose an axiomatic system ${\mathrm {BZFC}}$, obtained by analysing the ${\mathrm {ZFC}}$ -axioms and translating them to a four-valued setting in a careful manner, avoiding many of the obstacles encountered by other attempted formalizations. We introduce the anti-classicality axiom postulating the existence of non-classical sets, and prove a surprising results stating that the existence of a single non-classical set is sufficient to produce any other type of non-classical set. Our theory is naturally bi-interpretable with ${\mathrm {ZFC}}$, and provides a philosophically satisfying view in which non-classical sets can be seen as a natural extension of classical ones, in a similar way to the non-well-founded sets of Peter Aczel [1]. Finally, we provide an interesting application concerning Tarski semantics, showing that the classical definition of the satisfaction relation yields a logic precisely reflecting the non-classicality in the meta-theory. (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)

The main aim of this paper is to introduce first-order versions of logics of evidence and truth, together with corresponding sound and complete Kripke semantics with variable and constant domains. According to the intuitive interpretation proposed here, these logics intend to represent possibly inconsistent and incomplete information bases over time. The paper also discusses the connections between Belnap-Dunn’s and da Costa’s approaches to paraconsistency, and argues that the logics of evidence and truth combine them in a very natural way.

In this paper, Graham Priest’s understanding of dialetheism, the view that there exist true contradictions, is discussed, and various kinds of metaphysical dialetheism are distinguished between. An alternative to dialetheism is presented, namely a thesis called ‘dimathematism’. It is pointed out that dimathematism enables one to escape a slippery slope argument for dialetheism that has been put forward by Priest. Moreover, dimathematism is presented as a thesis that is helpful in rejecting the claim that logic is a normative discipline.

We develop a general theory of FDE-based modal logics. Our framework takes into account the four-valued nature of FDE by considering four partially defined modal operators corresponding to conditions for verifying and falsifying modal necessity and possibility operators. The theory comes with a uniform characterization for all obtained systems in terms of FDE-style formula-formula sequents. We also develop some correspondence theory and show how Hilbert-style axiom systems can be obtained in appropriate cases. Finally, we outline how different systems from the (...) literature can be expressed in our framework. (shrink)

In this article, I provide Urquhart-style semilattice semantics for three connexive logics in an implication-negation language (I call these “pure theories of connexive implication”). The systems semantically characterized include the implication-negation fragment of a connexive logic of Wansing, a relevant connexive logic recently developed proof-theoretically by Francez, and an intermediate system that is novel to this article. Simple proofs of soundness and completeness are given and the semantics is used to establish various facts about the systems (e.g., that two of (...) the systems have the variable sharing property). I emphasize the intuitive content of the semantics and discuss how natural informational considerations underly each of the examined systems. (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)

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)

In the paper Busaniche and Cignoli we presented a quasivariety of commutative residuated lattices, called NPc-lattices, that serves as an algebraic semantics for paraconsistent Nelson’s logic. In the present paper we show that NPc-lattices form a subvariety of the variety of commutative residuated lattices, we study congruences of NPc-lattices and some subvarieties of NPc-lattices.

In this paper, a way of constructing many-valued paraconsistent logics with weak double negation axioms is proposed. A hierarchy of weak double negation axioms is addressed in this way. The many-valued paraconsistent logics constructed are defined as Gentzen-type sequent calculi. The completeness and cut-elimination theorems for these logics are proved in a uniform way. The logics constructed are also shown to be decidable.

Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a sublogic of N4. Fifthly, a strong normalization theorem is (...) proved for a typed λ-calculus for a neighbor of N4. Finally, it is remarked that the natural deduction frameworks presented can also be adapted for Wansing's basic connexive logic C. (shrink)

Earlier algebraic semantics for Belnapian modal logics were defined in terms of twist-structures over modal algebras. In this paper we introduce the class of BK -lattices, show that this class coincides with the abstract closure of the class of twist-structures, and it forms a variety. We prove that the lattice of subvarieties of the variety of BK -lattices is dually isomorphic to the lattice of extensions of Belnapian modal logic BK . Finally, we describe invariants determining a twist-structure over a (...) modal algebra. (shrink)

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)

This paper deals with various substructural propositional logics, in particular with substructural subsystems of Nelson's constructive propositional logics N– and N. Doen's groupoid semantics is extended to these constructive systems and is provided with an informational interpretation in terms of information pieces and operations on information pieces.

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)

We investigate some non-normal variants of well-studied paraconsistent and paracomplete modal logics that are based on N. Belnap’s and M. Dunn’s four-valued logic. Our basic non-normal modal logics are characterized by a weak extensionality rule, which reflects the four-valued nature of underlying logics. Aside from introducing our basic framework of bi-neighbourhood semantics, we develop a correspondence theory in order to prove completeness results with respect to our neighbourhood semantics for non-normal variants of \, \ and \.

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...) BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm. (shrink)

We compare the logic HYPE recently suggested by H. Leitgeb as a basic propositional logic to deal with hyperintensional contexts and Heyting-Ockham logic introduced in the course of studying logical aspects of the well-founded semantics for logic programs with negation. The semantics of Heyting-Ockham logic makes use of the so-called Routley star negation. It is shown how the Routley star negation can be obtained from Dimiter Vakarelov’s theory of negation and that propositional HYPE coincides with the logic characterized by the (...) class of all involutive Routley star information frames. This result provides a much simplified semantics for HYPE and also a simplified axiomatization, which shows that HYPE is identical with the modal symmetric propositional calculus introduced by G. Moisil in 1942. Moreover, it is shown that HYPE can be faithfully embedded into a normal bi-modal logic based on classical logic. Against this background, we discuss the notion of hyperintensionality. (shrink)

Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...) N4C and N4C+ are proved. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

The purpose of this paper is to present a paraconsistent formal system and a corresponding intended interpretation according to which true contradictions are not tolerated. Contradictions are, instead, epistemically understood as conflicting evidence, where evidence for a proposition A is understood as reasons for believing that A is true. The paper defines a paraconsistent and paracomplete natural deduction system, called the Basic Logic of Evidence, and extends it to the Logic of Evidence and Truth. The latter is a logic of (...) formal inconsistency and undeterminedness that is able to express not only preservation of evidence but also preservation of truth. LETj is anti-dialetheist in the sense that, according to the intuitive interpretation proposed here, its consequence relation is trivial in the presence of any true contradiction. Adequate semantics and a decision method are presented for both BLE and LETj, as well as some technical results that fit the intended interpretation. (shrink)

Various four- and three-valued modal propositional logics are studied. The basic systems are modal extensions BK and BS4 of Belnap and Dunn's four-valued logic of firstdegree entailment. Three-valued extensions of BK and BS4 are considered as well. These logics are introduced semantically by means of relational models with two distinct evaluation relations, one for verification and the other for falsification. Axiom systems are defined and shown to be sound and complete with respect to the relational semantics and with respect to (...) twist structures over modal algebras. Sound and complete tableau calculi are presented as well. Moreover, a number of constructive non-modal logics with strong negation are faithfully embedded into BS4, into its three-valued extension B3S4, or into temporal BS4, BtS4. These logics include David Nelson's three-valued logic N3, the four-valued logic N4 bottom, the connexive logic C, and several extensions of bi-intuitionistic logic by strong negation. (shrink)

The Craig interpolation theorem is shown for an extended LJ with strong negation. A new simple proof of this theorem is obtained. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.