A New Algebraic Version of Monteiro’s Four-Valued Propositional Calculus ()
1. Preliminaries
In 1978,
A.
Monteiro introduced four-valued modal algebras as a generalization of 3-valued Łukasiewicz algebras. These algebras raise a genuine interest both from the points of view of algebra and logic, and especially from that of Algebraic Logic. It is worth mentioning that Monteiro expressed his view that in near future these algebras would give rise to a four-valued modal logic with significant applications in computer science. His insight was essentially right, although we don’t know if such applications have yet been developed. On the other hand, it is well known that Font and Rius (1990, 2000) have done an exhaustive research into four-valued modal logics. In particular, in ( Font & Rius, 1990 ) they studied the class of abstract logics projectively generated by the class of logics defined on four-valued modal algebras by the family of their filters and they obtained an axiomatization of them by means of a Gentzen calculus. Furthermore, in ( Font & Rius, 2000 ) they defined two sentential logics. One of them is algebrizable in the sense of ( Blok & Pigozzi, 1989 ) and the corresponding algebras are four-valued modal algebras. The other is not algebrizable in the above sense, but its algebraic counterpart is also the class of four-valued modal algebras. These results gave a positive answer to Monteiro’s conjecture. Besides, in ( Bianco, 2004, 2008 ) we gave a Hilbert-style propositional calculus, called four-valued Monteiro propositional calculus which we would describe below. An algebraic study of four-valued modal algebras can be found in ( Figallo et al., 1991, 1992, 1994, 1995 ) and ( Loureiro, 1980, 1983a, 1983b, 1983c, 1984, 1985 ). Recall that:
A four-valued modal algebra is an algebra
of type
such that the reduct
is a distributive lattice with greatest element 1 satisfying these conditions:
(L1)
,
(L2)
,
(L3)
,
(L4)
.
From the definition, it follows that A is a De Morgan algebra ( Monteiro, 1960; Birkhoff, 1967 ). Besides, Loureiro (1982, 1983a) proved que that the variety
of these algebras is generated by the algebra
, where
1)
is the De Morgan algebra such that
and
, being
not comparable;
2) The operation
is defined by
and
for all
.
In what follows, we will denote by
the category of four-valued modal algebras and their corresponding homomorphisms.
For the notions of universal algebra including distributive lattices, De Morgan algebras and category theory used in this paper we refer the reader to ( Kalman, 1958 ; Birkhoff, 1967 ; MacLane, 1971 ; Burris & Sankappana- var, 1981 ).
The structure of the paper is as follows: In Section 1, we develop a Hilbert-style propositional calculus which we call four-valued Monteiro propositional calculus and denote by
. Besides, we prove that
belongs to the class of standard systems of implicative extensional propositional calculi ( Rasiowa, 1974 ). Furthermore, we show that the notions of four-valued modal algebra and
-algebra are equivalent. Finally, we demonstrate that
is consistent and that the completeness theorem holds. From the equivalence established above, we conclude that from any algebra
we have that
is an
-algebra where
and
and conversely, from any
-algebra we obtain a four-valued modal algebra by defining
. These statements and the fact that
can be defined from
allow us to assert that
and the variety
generated by
are polynomially equivalent. In Section 2, we introduce the variety
of modal distributive lattices with implication and we show that the category
of these algebras and their corresponding homomorphisms is equivalent to
. Thus, the category theory notably simplify the proof that should be performed to obtain this result by direct calculations. Hence, we determine a new equational descrip- tion of four-valued modal algebras which is more convenient than the latter to study
from an algebraic point of view, since the implication
is one of its basic binary operations.
2. Four-Valued Monteiro Propositional Calculus
The main aim of this section is to describe the propositional calculus
and show that it has four-valued modal algebras as the algebraic counterpart. The terminology and symbols used here coincide in general with those used in ( Rasiowa, 1974 ).
Let
be a formalized language of zero order such that in the alphabet
the set
1)
of propositional variables which they will be denoted by
, is enumerable;
2)
is empty;
3) L1 contains two elements denoted by
and
called negation sign and modal operator sign, respectively;
4)
contains three elements denoted by
,
and
called conjunction sign, weak implication sign and implication sign, respectively;
5)
contains two elements denoted by
.
Let F be the set of all formulas over A0. For any
in
, we shall write for short
instead of
.
We assume that the set
of logical axioms consists of all formulas of the following form, where
are any formulas in
:
(A1)
,
(A2)
,
(A3)
,
(A4)
,
(A5)
,
(A6)
,
(A7)
,
(A8)
,
(A9)
,
(A10)
,
(A11)
,
(A12)
,
(A13)
,
(A14)
,
(A15)
,
(A16)
,
(A17)
,
(A18)
,
(A19)
,
(A20)
,
(A21)
,
(A22)
,
(A23)
,
(A24)
,
(A25)
,
(A26)
,
(A27)
,
(A28)
,
(A29)
,
(A30)
.
The consequence operation
in
is determined by the set
and by the following rule of inference:
(R1)
, (
Modus
Ponens
)
The system
thus obtained, will be called four-valued Monteiro propositional calculus. It is worth mentioning that the above connectives are not independent, however, we consider them for simplicity. We shall denote by
the set of all formulas derivable in
. As usual, if
we shall say that
is a theorem of
and we shall write
or
.
In Lemma 1.1 we summarize the most important rules and theorems necessary for further development.
Lemma 1.1. In
the following rules and theorems hold:
(R2)
,
(R3)
,
(T1)
,
(T2)
,
(R4)
,
(R5)
,
(R6)
,
(T3)
,
(T4)
,
(R7)
,
(R8)
,
(R9)
,
(R10)
,
(R11)
,
(R12)
,
(T5)
,
(R13)
,
(R14)
,
(T6)
,
(T7)
,
(T8)
,
(T9)
,
(T10)
,
(T11)
,
(R15)
,
(T12)
,
(T13)
,
(R16)
,
(T13)
,
(R17)
,
(R18)
,
(R19)
.
Proof. We only prove (R15), (R16) and (R17).
(R15):
1)
,
2)
, [(1), (R11), (A3), (r1)]
3)
, [(1), (R11), (A4), (r1)]
4)
, [(A7), (R4)]
5)
, [(3), (4), (r1)]
6)
, [(T11), (R4)]
7)
, [(3), (6), (r1)]
8)
, [(A9), (7), (R7)]
9)
. [(5), (8), (R9), (R12)]
(R16):
1)
,
2)
,
3)
, [(1), (R11), (A4)]
4)
, [(2), (R11), (A3)]
5)
, [(2), (R11), (A4)]
6)
, [(5), (A16), (r1)]
7)
, [(6), (T13), (r1)]
8)
, [(A18), (3), (4), (r1)]
9)
. [(7), (8), (R9), (R12)]
(R17):
1)
,
2)
,
3)
, [(1), (R11), (A3)]
4)
, [(2), (R11), (A3)]
5)
, [(2), (R11), (A4)]
6)
, [(T4), (3), (r1)]
7)
, [(T14), (3), (r1)]
8)
, [(T9)]
9)
, [(8), (T1), (r1)]
10)
, [(7), (A12), (R7)]
11)
, [(10), (A11), (R7)]
12)
, [(11), (9), (r1)]
13)
, [(6), (12), (R9), (R12)]
14)
, [(T2), (4), (r1)]
15)
, [(5), (R4)]
16)
, [(A11), (15), (R7)]
17)
, [(A12)]
18)
, [(16), (17), (R7)]
19)
, [(18), (A13), (R7)]
20)
, [(14), (19), (R9), (R12)]
21)
. [(13), (20), (R13)] □
Theorem 1.1. The propositional calculus
belongs to the class of standard systems of implicative extensional propositional calculi.
Proof. We have to prove that conditions (s1) to (s8) in ( Rasiowa, 1974 ) are satisfied. Clearly, (s1) and (s2) are verified. Besides, (s3), (s4), (s5) and (s6) follow from (T5), (R10), (R13) and (R14), respectively. On the other hand, taking into account (R15) and (R16), we have that (s7) holds. Finally, (R17), (R18) and (R19) allow us to conclude (s8). □
Next, our attention is focused on stating the relationship between four-valued modal algebras and
- algebras ( Rasiowa, 1974 ). Lemma 1.2 will be fundamental for this purpose.
Lemma 1.2. In
the following theorems hold:
(T15)
,
(T16)
,
(T17)
,
(T18)
,
(T19)
,
(T20)
.
(T21)
,
(T22)
,
(T23)
,
(T24)
,
(T25)
,
(T26)
,
(T27)
.
Proof. We only prove (T17), (T20), (T22) and (T27).
(T17):
1)
, [(A4)]
2)
, [(1), (R8)]
3)
, [(2), (R4)]
4)
, [(T16)]
5)
, [(4), (R4)]
6)
, [(3), (5), (r1)]
7)
, [(A2)]
8)
, [(7), (R6)]
9)
, [(A3), (8), (r1)]
10)
, [(9), (R4)]
11)
. [(6), (10), (r1)]
(T20):
1)
, [(A19)]
2)
, [(1), (R4)]
3)
, [(2), (T8), (r1)]
4)
, [(T7)]
5)
. [(3), (4), (R7)]
(T22):
1)
, [(T18)]
3)
, [(A3)]
4)
, [(T17)]
5)
, [(A10)]
6)
, [(4), (R2)]
7)
, [(3), (5), (r1)]
8)
, [(2), (6), (R9)]
9)
. [(7), (1), (r1)]
(T27):
1)
, [(T26)]
2)
, [(1), (R8)]
3)
, [(T7)]
4)
, [(3), (R4)]
5)
, [(4), (T25), (r1)]
6)
. [(5), (2), (r1)] □
Remark 1.1. It is worth noting that if
is a formula derivable in
, then
for every valua- tion
of
in every
-algebra
.
Proposition 1.1. Let
. Then
is an
-algebra, where
and
are defined as follows:
,
.
Proof. We shall prove that conditions (a1) to (a4) in ( Rasiowa, 1974 ) hold. Indeed, taking into account the definitions of
and
we have that (a1) and (a2) are satisfied. On the other hand, let
be such that
. Then, we get (1)
and (2)
. From (1), (A2) and (2), (A14) we have that
and
respectively. These assertions and the fact that
if and only if
and
allow us to conclude that
and so, (a3) holds. Besides, if
, then by an analogous argument to that used in the proof of (a3), we get
, from which we infer (a4). □
Proposition 1.2. Let
be an
-algebra. Then
where
.
Proof. To show that
is a De Morgan algebra, by ( Marona, 1964 ) it suffices to prove that conditions (M1)
and (M2)
are satisfied. By virtue of Remark 1.1 and (a4) in ( Rasiowa, 1974 ), (M2) follows from (A23) and (M1) from (A3), (A19), (T19), (T20), (R9) and (R12). Moreover, following an analogous reasoning and taking into account (A24) we infer (L3); besides, (T22), (T23), (T24), (T27), (R9) and (R12) allow us to conclude (L4). Hence, the proof is complete. □
From Propositions 1.1 and 1.2 we infer:
Theorem 1.2. The notions of
-algebra and four-valued modal algebra are equivalent.
Let
be the binary relation on
defined as follows:
if and only if
and
in
.
Then,
is a congruence relation on
and
determines an equivalence class which will be denoted by 1. Moreover,
is an
-algebra ( Rasiowa, 1974 ) and therefore from Proposition 1.2, we conclude:
Theorem 1.3.
.
On the other hand, since
is consistent, from ( Rasiowa, 1974 ) and Theorem 1.2 we have that the completeness theorem for
holds, which is included in.
Theorem 1.4. Let
be a formula of
. Then the following conditions are equivalent:
1)
is derivable in
;
2)
is valid in every
-algebra;
3)
, where
is the canonical valuation in the algebra
.
3. Categorical Equivalence between
and ![]()
In this section we introduce the notion of modal distributive lattice with implication and we prove some pro- perties of these algebras which allow us to show the announced categorical equivalence.
Definition 2.1. A modal distributive lattice with implication (or
-algebra) is an algebra
of type
where
is a bounded disitributive lattice satisfying the following identities:
(I1)
,
(I2)
,
(I3)
,
(I4)
,
(I5)
,
(I6)
,
(I7)
,
(I8)
,
(I9)
,
(I10)
,
(I11)
,
(I12)
.
In Proposition 2.1 we show some properties of
-algebras which will be useful in what follows.
Proposition 2.1. Let
be an
-algebra. Then the following identities hold:
(I13)
,
(I14)
,
(I15)
,
(I16)
,
(I17)
,
(I18)
,
(I19)
,
(I20)
,
(I21)
,
(I22)
,
(I23)
,
(I24)
implies
,
(I25)
implies
,
(I26)
if and only if
,
,
(I27)
implies
,
(I28)
,
(I29)
.
Proof. We only prove (I22) and (I26).
(I22): From (I21), (I5), (I3) and (I12) we have that
.
(I26): Let
. Then, from (I4), (I1), and (I14) we conclude that
. Besides, (I1) allows us to infer
. Conversely, from the hypothesis, (I13) and (I12) we have that
, and so,
. □
Let
be an
-algebra. Then, we define
, where
for every
. Furthermore, given the
-algebras
,
and a homo- morphism
, we define
by
.
Lemma 2.1 and Propositions 2.2, 2.3 and 2.4 are fundamental in order to prove Theorem 2.1.
Lemma 2.1. Let
be an
-algebra. Then the following properties are verified:
(I30)
,
(I31)
,
(I32)
,
(I33)
,
(I34)
,
(I35)
,
(I36)
implies
,
(I37)
implies
,
(I38)
,
(I39)
implies
.
Proof. We only prove (I30) and (I39).
(I30): From (I5), (I17), (I20) and (I4) we have that
and
. Besides, (I23), (I6) and (I1) allow us to infer that
. In addition, from (I8), (I23), (I6) and (I26) we have
. By these assertions and (I26) we conclude the proof.
(I39): From (I4), (I5) and (I31) we get that
.
Then, by (I21), (I36), (I14) and (I2) we conclude that
. On the other hand, from (I35), (I38), (I19) and (I36) we have that
. Hence, the above assertions and (I26) allow us to conclude that
. □
Proposition 2.2.
is a four-valued modal algebra.
Proof. We only have to prove that
satisfies conditions (L1)-(L4).
(L1): Taking into account (I34), (I33), (I8) and (I15) we infer that
.
then, by (I19), (I21), (I3) and (I30) we have that
.
(L2): It is a direct consequence of (I39) and (L1).
(L3): From (I23) and (I10) we conclude that
. This identity and (I10) allow us to infer that
.
(L4): It follows from (I6) and (I30). □
Proposition 2.3.
is a full and faithful functor between
-algebras and four-valued modal algebras.
Proof. It follows from Proposition 2.2 and the definition of
. □
Proposition 2.4. Every four-valued modal algebra
is isomorphic (equal) to
for some
-algebra
.
Proof. Let
, where
for all
. As properties (I1)-(I12) hold in
, then
is an
-algebra. In order to complete the proof, we must show that
. If we de- fine
, by Proposition 2.2 it follows that
is a four-valued modal algebra. In addition, for every
,
, since this identity holds in
. □
Theorem 2.1.
is a categorical equivalence between
and
.
Proof. It is a direct consequence of Propositions 2.3, 2.4 and Theorem 1 of ( MacLane, 1971 ). □
Theorem 2.1 and the results on Section 1 confirm that
-algebras are the algebraic counterpart of the four-valued Monteiro propositional calculus.