Bilattices with implications (Q368472)

A bilattice is an algebra \(\mathbf{B} = \langle B, \land,\lor,\otimes,\oplus, \neg \rangle\) such that the reducts \(\langle B,\land, \lor \rangle\) and \(\langle B,\otimes,\oplus, \rangle\) are both lattices and the negation \(\neg\) is a unary operation anti-monotone relative to both orders and such that for every \(a \in B\) we have \(a = \neg \neg a\). A Brouwerian bilattice is a bilattice endowed with an implication \(\supset\) satisfying the following conditions: (B1) \((x \supset x)\supset y \approx y\) (B2) \(x \supset (y \supset z) \approx (x \land y) \supset z \approx (x \otimes y) \supset z\) (B3) \((x \lor y) \supset z \approx (x \supset z) \land (y \supset z) \approx (x \oplus y) \supset z\) (B4) \(x \land ((x \supset y) \supset (x \otimes y)) \approx x\) (B5) \(\neg (x \supset y) \supset z \approx (x \land \neg y) \supset z\). It is proved that a variety of Brouwerian bilattices forms an exact algebraic semantics of the logic \(\mathcal{B}\), introduced in Section 1 of the paper by a Hilbert-style calculus. Theorem 2.12 describes all reduced logical matrices that are models of the logic \(\mathcal{B}\) in the following way: A matrix \(\langle \mathbf{A}, D \rangle\) is a reduced model of \(\mathcal{B}\) (or of \(\mathcal{B}\) plus Pierce's law) if and only if \(\mathbf{A}\) is a Brouwerian (or a classical implicative) bilattice and \(D = \{ a \in A: a = a \supset a\}\).