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)

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.

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)