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.

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)

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.

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 QNc5, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QNc5, 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. (shrink)

Da Costa's C systems are surveyed and motivated, and significant failings of the systems are indicated. Variations are then made on these systems in an attempt to surmount their defects and limitations. The main system to emerge from this effort, system CC , is investigated in some detail, and dual-intuitionistic semantical analyses are developed for it and surrounding systems. These semantics are then adapted for the original C systems, first in a rather unilluminating relational fashion, subsequently in a more illuminating (...) way through the introduction of impossible situations where and and or change roles. Finally other attempts to break out of impasses for the original and expanded C systems, by going inside them, are looked at, and further research directions suggested. (shrink)

In this paper, the positive fragment of the logic math formula of contraction-less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four-valued logic math formula. This extended relevant logic is called math formula, and it has the property of constructible falsity which is known to be a characteristic property of math formula. A Gentzen-type sequent calculus math formula for math formula is introduced, and the cut-elimination and decidability (...) theorems for math formula are proved. Two extended Routley-Meyer semantics are introduced for math formula, and the completeness theorems with respect to these semantics are proved. (shrink)

Our paper aims to investigate inference rules for Nelson’s logics and to discuss possible ways to determine admissibility of inference rules in such logics. We will use the technique offered originally for intuitionistic logic and paraconsistent minimal Johannson’s logic. However, the adaptation is not an easy and evident task since Nelson’s logics do not enjoy replacement of equivalences rule. Therefore we consider and compare standard admissibility and weak admissibility. Our paper founds algorithms for recognizing weak admissibility and admissibility itself – (...) for restricted cases, to show the problems arising in the course of study. (shrink)

It was proved by Odintsov and Pearce that the logic is a deductive base for paraconsistent answer set semantics of logic programs with two kinds of negation. Here we describe the lattice of logics extending, characterise these logics via classes of -models, and prove that none of the proper extensions of is a deductive base for PAS.

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

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)

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)

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.

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

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 examine some extensions of the constructive propositional logic with strong negation in the setting of varieties of $\mathcal{N}$ -lattices. The main aim of the paper is to give a description of all pretabular, primitive and preprimitive varieties of $\mathcal{N}$ -lattices.