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 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)