Paraconsistent quantum logics are weak forms of quantum logic, where the noncontradiction and the excluded-middle laws are violated. These logics find interesting applications in the operational approach to quantum mechanics. In this paper, we present an axiomatization, a Kripke-style, and an algebraic semantical characterization for two forms of paraconsistent quantum logic. Further developments are contained in Giuntini and Greuling's paper in this issue.

In their useful logic for a computer network Shramko and Wansing generalize initial values of Belnap’s 4-valued logic to the set 16 to be the power-set of Belnap’s 4. This generalization results in a very specific algebraic structure — the trilattice SIXTEEN 3 with three orderings: information, truth and falsity. In this paper, a slightly different way of generalization is presented. As a base for further generalization a set 3 is chosen, where initial values are a — incoming data is (...) asserted, d — incoming data is denied, and u — incoming data is neither asserted nor denied, that corresponds to the answer “don’t know”. In so doing, the power-set of 3, that is the set 8 is considered. It turns out that there are not three but four orderings naturally defined on the set 8 that form the tetralattice EIGHT 4 . Besides three ordering relations mentioned above it is an extra uncertainty ordering. Quite predictably, the logics generated by a –order (truth order) and d –order (falsity order) coincide with first-degree entailment. Finally logic with two kinds of operations ( a –connectives and d –connectives) and consequence relation defined via a –ordering is considered. An adequate axiomatization for this logic is proposed. (shrink)

The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. (...) The outcome are paraconsistent logics with a lot of desirable properties.1. (shrink)

Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is (...) addressed. (shrink)

Lattice logic, bilattice logic, and paraconsistent quantum logic are investigated based on monosequent systems. Paraconsistent quantum logic is an extension of lattice logic, and bilattice logic is an extension of paraconsistent quantum logic. Monosequent system is a sequent calculus based on the restricted sequent that contains exactly one formula in both the antecedent and succedent. It is known that a completeness theorem with respect to a lattice-valued semantics holds for a monosequent system for lattice logic. A completeness theorem with respect (...) to a lattice-valued semantics is proved for paraconsistent quantum logic, and a completeness theorem with respect to a bilattice-valued semantics is proved for bilattice logic. Some syntactical properties, including cut-elimination and duality, are also investigated for the monosequent systems for these logics. (shrink)

In this paper we present a solution of the axiomatization problem for the Fmla-Fmla versions of the Pietz and Rivieccio exactly true logic and the non-falsity logic dual to it. To prove the completeness of the corresponding binary consequence systems we introduce a specific proof-theoretic formalism, which allows us to deal simultaneously with two consequence relations within one logical system. These relations are hierarchically organized, so that one of them is treated as the basic for the resulting logic, and the (...) other is introduced as an extension of this basic relation. The proposed bi-consequences systems allow for a standard Henkin-style canonical model used in the completeness proof. The deductive equivalence of these bi-consequence systems to the corresponding binary consequence systems is proved. We also outline a family of the bi-consequence systems generated on the basis of the first-degree entailment logic up to the classic consequence. (shrink)

In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems (...) for classical logic and Girard's proofnets for linear logic. (shrink)

It will be an essential resource for philosophers, mathematicians, computer scientists, linguists, or any scholar who finds connectives, and the conceptual issues surrounding them, to be a source of interest.This landmark work offers both ...

In this paper we present a solution of the axiomatization problem for the Fmla-Fmla versions of the Pietz and Rivieccio exactly true logic and the non-falsity logic dual to it. To prove the completeness of the corresponding binary consequence systems we introduce a specific proof-theoretic formalism, which allows us to deal simultaneously with two consequence relations within one logical system. These relations are hierarchically organized, so that one of them is treated as the basic for the resulting logic, and the (...) other is introduced as an extension of this basic relation. The proposed bi-consequences systems allow for a standard Henkin-style canonical model used in the completeness proof. The deductive equivalence of these bi-consequence systems to the corresponding binary consequence systems is proved. We also outline a family of the bi-consequence systems generated on the basis of the first-degree entailment logic up to the classic consequence. (shrink)

Four-valued semantics proved useful in many contexts from relevance logics to reasoning about computers. We extend this approach further. A sequent calculus is defined with logical connectives conjunction and disjunction that do not distribute over each other. We give a sound and complete semantics for this system and formulate the same logic as a tableaux system. Intensional conjunction and its residuals can be added to the sequent calculus straightforwardly. We extend a simplified version of the earlier semantics for this system (...) and prove soundness and completeness. Then, with some modifications to this semantics, we arrive at a mathematically elegant yet powerful semantics that we call generalized Kripke semantics. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

In Belnap's useful 4-valued logic, the set 2 = {T, F} of classical truth values is generalized to the set 4 = ������(2) = {Ø, {T}, {F}, {T, F}}. In the present paper, we argue in favor of extending this process to the set 16 = ᵍ (4) (and beyond). It turns out that this generalization is well-motivated and leads from the bilattice FOUR₂ with an information and a truth-and-falsity ordering to another algebraic structure, namely the trilattice SIXTEEN₃ with an (...) information ordering together with a truth ordering and a (distinct) falsity ordering. Interestingly, the logics generated separately by the algebraic operations under the truth order and under the falsity order in SIXTEEN₃ coincide with the logic of FOUR₂, namely first degree entailment. This observation may be taken as a further indication of the significance of first degree entailment. In the present setting, however, it becomes rather natural to consider also logical systems in the language obtained by combining the vocabulary of the logic of the truth order and the falsity order. We semantically define the logics of the two orderings in the extended language and in both cases axiomatize a certain fragment comprising three unary operations: a negation, an involution, and their combination. We also suggest two other definitions of logics in the full language, including a bi-consequence system. In other words, in addition to presenting first degree entailment as a useful 16-valued logic, we define further useful 16-valued logics for reasoning about truth and (non-)falsity. We expect these logics to be an interesting and useful instrument in information processing, especially when we deal with a net of hierarchically interconnected computers. We also briefly discuss Arieli's and Avron's notion of a logical bilattice and state a number of open problems for future research. (shrink)

This article addresses and resolves some issues of relational, Kripke-style, semantics for the logics of bounded lattice expansions with operators of well-defined distribution types, focusing on the case where the underlying lattice is not assumed to be distributive. It therefore falls within the scope of the theory of Generalized Galois Logics, introduced by Dunn, and it contributes to its extension. We introduce order-dual relational semantics and present a semantic analysis and completeness theorems for non-distributive lattice logic with n -ary additive (...) or multiplicative operators, with negation operators modally interpreted as impossibility and unnecessity, as well as with implication connectives. Order-dual relational semantics shares with the generalized Kripke frames, or the bi-approximation semantics approach, the use of both a satisfaction and a co-satisfaction relation, but it also responds to the recently voiced concerns of Craig, Haviar and Conradie about the relative non-intuitiveness of the 2-sorted semantics of the aforementioned approaches. In this article, we provide a standard interpretation of modalities and natural interpretations of both negation and implication, despite the absence of distribution. Thereby, our results contribute in creating the necessary background for research in non-distributive logics with modalities variously interpreted as dynamic, temporal etc, by analogy to the classical case. (shrink)

In their useful logic for a computer network Shramko and Wansing generalize initial values of Belnap’s 4-valued logic to the set 16 to be the power-set of Belnap’s 4. This generalization results in a very specific algebraic structure — the trilattice SIXTEEN3 with three orderings: information, truth and falsity. In this paper, a slightly different way of generalization is presented. As a base for further generalization a set 3 is chosen, where initial values are a — incoming data is asserted, (...) d — incoming data is denied, and u — incoming data is neither asserted nor denied, that corresponds to the answer “don’t know”. In so doing, the power-set of 3, that is the set 8 is considered. It turns out that there are not three but four orderings naturally defined on the set 8 that form the tetralattice EIGHT4. Besides three ordering relations mentioned above it is an extra uncertainty ordering. Quite predictably, the logics generated by a–order and d–order coincide with first-degree entailment. Finally logic with two kinds of operations and consequence relation defined via a–ordering is considered. An adequate axiomatization for this logic is proposed. (shrink)

This paper is a reaction to the following remark by grzegorczyk: "the compound sentences are not a product of experiment. they arise from reasoning. this concerns also negations; we see that the lemon is yellow, we do not see that it is not blue." generally, in science the truth is ascertained as indirectly as falsehood. an example: a litmus-paper is used to verify the sentence "the solution is acid." this approach gives rise to a (very intuitionistic indeed) conservative extension of (...) the heyting logic satisfying natural duality laws. (shrink)