Many-Valued Modal Logics

Melvin C. Fitting
Department of Mathematics and Computer Science
Lehman College (CUNY)
Bedford Park Boulevard West
Bronx, NY 10468, USA
MLFLC@[Link]

Abstract. Two families of many-valued modal logics are investigated. Semantically, one family is characterized using Kripke models that allow formulas to
take values in a finite many-valued logic, at each possible world. The second family generalizes this to allow the accessibility relation between worlds also to be
many-valued. Gentzen sequent calculi are given for both versions, and soundness
and completeness are established.

Introduction

The logics that have appeared in artificial intelligence form a rich and varied collection.
While classical (and maybe intuitionistic) logic suffices for the formal development
of mathematics, artificial intelligence has found uses for modal, temporal, relevant,
and many-valued logics, among others. Indeed, I take it as a basic principle that an
application should find (or create) an appropriate logic, if it needs one, rather than
reshape the application to fit some narrow class of established logics. In this paper I
want to enlarge the variety of logics available by introducing natural blendings of modal
and many-valued logics.
Many-valued modal logics have been considered before [12, 13, 11, 6, 8, 7], but
perhaps in too narrow a sense. The basic idea was to retain the general notion of
possible world semantics, while allowing formulas to have values in a many-valued
space, at each possible world. What seems not to have been considered is allowing
the accessibility relation between possible worlds itself to be many-valued. But manyvalued accessibility is a very natural notion. After all, some worlds alternative to this
one are more relevant, others less, as one intuitively thinks of these things.
The general plan of the paper is as follows. In order to have a suitable prooftheoretic framework on which to build, I begin with a many-valued sequent calculus,
allowing a uniform approach to a rich family of finitely many-valued logics. This calculus
is new, quite different from the approach in [10], and may be of some independent
interest. Completeness is established. Then two families of many-valued modal logics
are introduced. In semantic terms, one family requires the accessibility relation to be
classical; the other allows it to be many-valued. For both families, sequent calculus
formulations are presented, and completeness is shown.

Basic Syntax and semantics

Before modal issues can be discussed, a multiple-valued framework must be erected

on which to build. I want to keep things as general as I can manage, and so I begin
with a space of truth values that constitutes a finite lattice nothing more. This
means there are natural notions of conjunction and disjunction, but not necessarily
of negation. Implication plays an intermediate role: it is allowed, and interpreted by
the partial ordering of the lattice of truth values, but in general it can not be nested.
However, for certain special categories of lattices a natural notion of nestable implication
is possible I treat such things separately, after dealing with the more general case.
Notation For the rest of this paper, T is a finite lattice. Its members are referred to
as truth values. The lattice ordering is denoted , and the meet and join operations by
and . The bottom and the top of T are denoted false and true respectively, and it
is assumed that false 6= true.
Next a logical language, relative to T , is specified. It was observed above that
implications will not generally be nestable, so there are two categories of compound
expressions: formulas, and implications between formulas. In classical two-valued logic,
P P and P P serve to define within the language counterparts of false and true.
In multiple-valued logics as general as those being considered now, the basic machinery
may not be enough to define counterparts of all truth values, and so propositional
constants are explicitly added to the language. To keep things simple, just assume
members of T themselves can be used as atomic formulas. Now for the details.
Definition 2.1 The propositional language LT is specified as follows:
Atomic formulas of LT are propositional variables, denoted P , Q, etc., and propositional constants, which are members of T .
Formulas of LT are built up as follows. Atomic formulas of LT are formulas of
LT . If A and B are formulas of LT , so are (A B) and (A B).
Implications of LT are expressions of the form (A B) where A and B are
formulas.
For reading convenience: formulas are denoted A, B, etc.; implications are denoted X,
Y , etc.; sets of implications are denoted , , etc. Also, , X will be used to abbreviate
{X}, and similarly for other set-theoretic combinations. Finally, parentheses in
formulas and implications will often be omitted.
In later sections the set of formulas will sometimes be closed under implication. But
whether this is the case or not, implications are the basic unit of currency. Now for
semantic issues.
Definition 2.2 A valuation is a mapping from atomic formulas of LT to T that maps
each member of T to itself.
If v is a valuation, its action is extended to all formulas in the obvious way: v(A B) =
v(A) v(B), where the on the right is the meet of T . Similarly for . Then
v(A) T if A is a formula of LT . Finally, implications of LT are mapped to T so
that v(A B) = true if and only if v(A) v(B). (If v(A) 6 v(B), the exact value
of v(A B) will not matter for now anything except true will do. Something more
explicit will be said when nestable implication is considered.)

A Many-valued proof procedure

Most many-valued proof procedures in the literature have been axiomatic, [10] for
instance. Here a somewhat unusual Gentzen-type sequent calculus will be introduced.
Unlike most sequent calculi, to the left and the right of the sequent arrow will be sets
of implications. Still, the underlying idea is the usual one.
Definition 3.1 is valid if, for every valuation v, either some member of is
not true under v, or some member of is true under v.
In most cases it is straightforward to check that each of the axioms below is valid,
and the rules preserve validity. Proofs are omitted. The usual structural rules come
first.
Identity Axiom
XX
Thinning

0 0

Cut

, X , X

Cut applications will generally be combined with Thinning, without comment. Next
are the rules for implication. The first is a transitivity axiom.
Axiom of Transitivity
X Y, Y Z X Z
Proposition 3.2 The following are derived rules:
, C A , C B
, A B
, B C , A C
, A B
Proof An argument for the first rule is given; the second is similar.
, C A C A, A B C B
Cut
, A B , C B
, C B
Cut
, A B

Next are two important rules for implication, making use of the truth values of T .
Rule RI

, t A , t B (for every t T )
, A B

Rule RI

, B t , A t (for every t T )
, A B

Here is the simple justification for the first of these rules; the second is treated in a
similar way. Suppose the sequent below the line is not valid. Say the valuation v maps
every member of to true, but does not map any member of , A B to true. In
particular, v(A) 6 v(B). Let t T be v(A). Then v maps every member of , t A to
true, but does not map any member of , t B to true, so one of the sequents above
the line is not valid.
It is interesting to observe what the rules above say for classical logic. Here there are
only two truth values. In Rule RI , when t is false, the sequent , t A , t B
is trivially obtainable, assuming false B. Thus only the t = true case is significant.
If A is identified with true A, Rule RI degenerates, in the classical case, to
, A , B
, A B
which is one of the usual classical sequent rules for implication. Rule RI can be
interpreted in a similar way, yielding a kind of contrapositive version of the rule.
There are more rules and axioms to come, but there are some results that can be
established now.
Proposition 3.3 For every formula A, A A
Proof Let t be an arbitrary member of T . Then t A t A, by Identity, so
A A, by RI .
Proposition 3.4 With Rules RI and RI available, the Axiom of Transitivity
follows from either of the Rules of Proposition 3.2.
Proof Transitivity is shown to follow from the first of the rules; the other is similar.
Let t be an arbitrary member of T .
tAtA
tBtB
thinning
thinning
t A t C, t B, t A
t A, t B t C, t B
Prop 3.2
t A, A B t C, t B (sequent one)

tCtC
tCtC
thinning
thinning
t A, t C t C, t A
t A, t C, t B t CA
Prop 3.2
A B, t A, t C t C (sequent two)
(sequent one) (sequent two)
Prop 3.2
A B, B C, t A t C
RI
A B, B C A C

Next are the expected lattice-theoretic rules for the lattice-theoretic connectives.

Conjunction Axioms
AB A
AB B
C A, C B C A B
Disjunction Axioms
AAB
B AB
A C, B C A B C
From the axioms above, the usual properties of the connectives follow; details are
omitted. Finally, rules that reflect the properties of T itself.
Propositional Constant Axioms
a b if a b
a b if a 6 b
Proposition 3.5 For any formula A, A true and false A.
Proof Again only the first is proved. Let t T be arbitrary.
t true
thinning
t A t true
RI
A true

Finally suppose an upward closed set of designated values, say {d1 , . . . , dk }, is specified in the usual multiple-valued logic style. Then the Gentzen calculus equivalent
of A being a tautology of the multiple-valued logic is the provability of the sequent
d1 A, . . . , dk A.

Many-valued completeness

Soundness of the sequent calculus is immediate. Completeness depends critically on a

derived rule, which we state below as Theorem 4.1. Proof of this theorem can be found
in the Appendix.
Theorem 4.1 The following is a derived rule:
, A t, t A (for all t T )

Using Theorem 4.1, completeness can be established by a fairly standard Lindenbaumstyle argument.

Definition 4.2 Let X be an implication, and let S be a set of implications. Say S is

X-inconsistent if, for some finite S, there is a proof of the sequent X. Also S
is X-consistent if it is not X-inconsistent.
In the usual way, an X-consistent set can be extended to a maximal X-consistent
one. And, as usual, it follows from the Cut Rule that if S is maximal X-consistent and
Y for some S, then Y S.
Proposition 4.3 Suppose S is a maximal X-consistent set. Then, for each formula A
there is exactly one a T such that both a A and A a are in S.
Proof First, it can not happen that a A, A a, b A and A b are all in S, for
a 6= b, because if a 6 b say, then
a A, A b a b a b
Cut
a A, A b
from which the X-inconsistency of S follows by Thinning.
Second, suppose that for no a T do we have a A and A a in S. Then (using
the finiteness of T ) there must be a finite set S such that , A a, a A X
is provable, for every a T . Then by Theorem 4.1, X is provable, contradicting
the X-consistency of S.
Now, suppose X is not provable. Then is X-consistent extend it to a maximal
X-consistent set, S. Define a valuation v as follows: for an atomic formula A set v(A)
to be that unique a T such that both A a and a A are in S. It is straightforward
to check that, for every formula F , v(F ) is the unique member f T such that F f
and f F are in S.
Say X is the implication A B, where v(A) = a and v(B) = b. If a b then S
would be X-inconsistent, by the following:
A a, b B, a b A B a b
Cut
A a, b B A B
Consequently a 6 b, so v(X) = v(A B) is not true. The following has now been
established.
Theorem 4.4 If an implication X is true under every valuation, X is provable in the
sequent calculus.

Nested implication

Up till now implication has been interpreted by a lattice ordering, and so an implication
is either true or it isnt, and thats all that has mattered. If implication is to be nestable,
something more elaborate is needed, and this requires more structure than just that of
a lattice. Here one way of dealing with this is presented other ways may be possible.
Definition 5.1 LT [] is the language defined like LT , but with the extra formation
rule: if A and B are formulas, so is A B (note that now implications are special kinds
of formulas).

There are several notions of implication that have been studied in multiple-valued
logics. Here one particular family that has nice mathematical properties is considered.
No claim is made that it is best for all applications. Proof theoretically, the laws of
importation and exportation are assumed. Semantically, the basic notion is that of
relative pseudo-complement from the algebraic semantics of intuitionistic logic, [9].
Definition 5.2 An element c T is the pseudo-complement of a relative to b if c is
the greatest member of T such that a c b. If the pseudo-complement of a relative
to b exists, it is denoted by a b. If relative pseudo-complements always exist, T is
said to have a relative pseudo-complement operation.
For finite lattices, having a relative pseudo-complement operation is equivalent to
being distributive. Thus the class with such an operation is a large and natural one. If
T has a relative pseudo-complement operation, valuations can be extended to formulas
of LT [] by setting v(A B) = v(A) v(B). This is compatible with the earlier
interpretation of implication that could not be nested, since one can show that when
the relative pseudo-complement operation is meaningful, a b = true if and only if
a b, see [9].
Since finite lattices are the only ones considered here, a bottom element always
exists; it has been denoted false throughout. A relatively pseudo-complemented lattice
with a bottom is called a pseudo-boolean algebra. Such algebras play a significant role
in the algebraic semantics of intuitionistic logic, though this is not an important issue
here.
Proof-theoretically, the sequent calculus is extended by adding the following rules.
Implication Axioms
(A B) C A (B C)
A (B C) (A B) C
The completeness proof extends easily; details are omitted.

An Example

Two versions of many-valued modal logic will be presented. The first version is the
most direct generalization of conventional modal logic. Before presenting the technical
details, a special case of considerable importance may help to motivate what follows.
Suppose hG, Ri is a frame in the usual modal sense: G is a non-empty set of possible
worlds, and R is a binary accessibility relation on G. Generally this is converted into
a model by adding an interpretation v, mapping possible worlds and atomic formulas
to (classical) truth values. Then v is extended to all formulas in the customary way,
in particular setting v(w, 2A) to be true just in case v(w0 , A) = true for all w0 G for
which wRw0 . It follows that v(w, 2A) = false if v(w0 , A) = false for some w0 G with
wRw0 .
Now imagine that the interpretation v is allowed to be partial; at each world it maps
some atomic formulas to true, others to false, and is undefined on still others. What is
a natural way of extending the incomplete information contained in v to all formulas?

For the classical connectives this is straightforward. A B should be taken to be true

at a world if both A and B are true there, and false if one of them is false. This leaves
A B without a truth value in all other cases; for instance, if A is true but B lacks a
truth value. See [1] for an extensive treatment of this partial logic.
The modal case can be dealt with along the same lines. Set v(w, 2A) = true if
v(w0 , A) = true for all w0 G such that wRw0 . Set v(w, 2A) = false if v(w0 , A) = false
for some w0 G with wRw0 . Otherwise v(w, 2A) is undefined. Then, for instance, if
there is some w0 G with wRw0 such that v(w0 , A) is undefined, and at all other worlds
alternate to w, A evaluates to true, then v(w, 2A) will be undefined. A treatment
of partial modal logic along these lines was suggested by Kripke in [5], where it was
observed that his theory of truth could be extended naturally to it.
In order to fit partial modal logic into the present treatment the obvious approach
is to treat the undefined case as if it were a third truth value. For the propositional
connectives this yields a well known three-valued logic, generally called Kleenes strong
three-valued logic, [4]. This logic can be presented most simply here by taking T =
{false, , true}, with the ordering false true. The third value, , can be read as
unknown or undetermined.
Incidentally, in Kleenes logic negation plays a major role, though it has not been
discussed here so far. The negation operation switches false and true, and leaves
unchanged. It can be introduced into the Gentzen system here very simply. Add a
unary operator, , and require the set of formulas to be closed under it. And add the
following six obvious axioms.
true false false true


false true true false
Now, what about the modal operator? The following is the three-valued version
of the partial semantics sketched above. Take a valuation, v, to be a mapping from
possible worlds and atomic formulas to the set {false, , true}. Extend it to all formulas
by evaluating , and at each world according to Kleenes logic, and using the
following for the modal case:
v(w, 2A) =

{v(w0 , A) | wRw0 }.

Such an approach has been considered before, for instance in [13, 11] (in the latter, however, the underlying three-valued logic is one due to L
ukasiewicz). In the next
section we present the semantics in detail, and give an appropriate corresponding modification to the Gentzen system.

Many-valued modal logic, version I

In this section the technical details of a family of many-valued modal logics are presented, both via semantics and a Gentzen system. For starters, the syntax is extended
in the obvious way. Throughout this section T is an arbitrary finite lattice, possibly
distributive.
Definition 7.1 LT [2] is the language defined like LT , but with the extra formation
rule: if A is a formula, so is 2A. Likewise LT [2, ] allows closure of the set of formulas

under both 2 and .

As was remarked earlier, the semantics is a direct modification of conventional possible world models.
Definition 7.2 A binary modal model is a structure hG, R, vi where G is a non-empty
set of possible worlds, R is a (classical, two-valued) relation on G, and v maps worlds
and atomic formulas to T , subject to the usual condition that members of T map to
themselves.
The mapping v is extended to all formulas in the usual way, with the special condition:
v(w, 2A) =

{v(w0 , A) | wRw0 }

It is easy to see that if T is the two-valued lattice of classical logic, this semantics collapses to the usual Kripke version. Also, the necessity operator has been considered only
a possibility operator could also be introduced, with the semantic characterization:
v(w, A) =

{v(w0 , A) | wRw0 }.

This operator will not be investigated here.

Corresponding to the notion of possible world model is the following rule of inference.
Binary Necessitation Rule For a1 , . . . , an , b T , and formulas A1 , . . . , An , B (n
may be 0):
a1 A1 , . . . , an An b B
a1 2A1 , . . . , an 2An b 2B
The validity of this rule will be discussed in the next section. Here are a few of the
formal consequences of the rule.
Proposition 7.3
1. for each t T , t 2t
AB
2. 2A 2B
3. (2A 2B) 2(A B)
4. 2(A B) (2A 2B)
Proof Item 1 is immediate from the Binary Necessitation Rule and t t. For item
2 take t to be an arbitrary member of T . Then:
t A, A B t B A B
Cut
t A t B Binary Necessitation
t 2A t 2B
RI
2A 2B
Proofs of items 3 and 4 are omitted.
Now suppose nested implications are allowed, using the language LT [2, ], and the
rules from Section 5. Then several additional items of interest can be proved.

Proposition 7.4 Let a be a member of T and A be an arbitrary formula. Then:

1. (a 2A) 2(a A);
2. 2(a A) (a 2A).
Proof The proof of item 1, slightly abbreviated, is as follows. Let t T be arbitrary.
Then beginning with an Implication Axiom:
(t a) A t (a A)
Binary Necessitation
(t a) 2A t 2(a A)
Implication Axiom
t (a 2A) t 2(a A)
RI
(a 2A) 2(a A)
The proof of part 2 is simpler, uses items from Proposition 7.3, and is omitted.
Next is a result that appears as a variation on the Binary Necessitation Rule its
significance will appear in a later section.
Theorem 7.5 For a1 , . . . , an , b T , and formulas A1 , . . . , An , B:
(a1 A1 . . . an An ) (b B)
(a1 2A1 . . . an 2An ) (b 2B)
Proof This follows easily from the preceeding two propositions.

Soundness and Completeness

The soundness of the Binary Necessitation Rule is straightforward. Suppose

a1 A1 , . . . , an An b B
is valid in all binary modal models. And suppose hG, R, vi is a model, and w G is a
world such that for i = 1, . . . , n, v(w, ai 2Ai ) = true. Then ai = v(ai ) v(2Ai ),
and by the conditions on 2 in binary modal models, for each w0 T with wRw0 ,
ai v(w0 , Ai ), so that v(w0 , ai Ai ) = true. Then by the assumption above, v(w0 , b
B) = true, so b v(w0 , B). Since this is the case for each such w0 , it follows that
b v(w, 2B), and so v(w, b 2B) = true. Thus the validity of the following has been
established
a1 2A1 , . . . an 2An b 2B.
Completeness, as usual, is more work, though the non-modal many-valued argument
extends directly.
Theorem 8.1 The modal system with the Binary Necessitation Rule is complete with
respect to binary modal models.
Proof Most of the details are omitted. Take G to be the collection of all maximal
X-consistent sets, for all implications X. For each w G and each formula A, set
v0 (w, A) to be the unique a T such that A a and a A are in w. For w, w0 G,

set wRw0 if v0 (w, 2A) v0 (w0 , A) for all formulas A. Finally, set v(w, A) = v0 (w, A)
for atomic A.
The key item to be verified is that v and v0 agree on all formulas, not just on the
atomic ones. This is done by an induction on degree. Only one case is presented:
consider the formula 2A, and assume the result is known for A.
1) If wRw0 then v0 (w, 2A) v0 (w0 , A). So
V

v0 (w, 2A)
{v0 (w0 , A) | wRw0 }
V
=
{v(w0 , A) | wRw0 }
= v(w, 2A)
2) Suppose v(w, 2A) 6 v0 (w, 2A). Set w00 = {v0 (w, 2C) C | all formulas C}.
Then w00 is v(2A) A-consistent, for otherwise, for some v0 (w, 2Ci ) Ci in w00 , we
would have:
v0 (w, 2C1 ) C1 , . . . , v0 (w, 2Cn ) Cn v(w, 2A) A
so by Binary Necessitation,
v0 (w, 2C1 ) 2C1 , . . . , v0 (w, 2Cn ) 2Cn v(w, 2A) 2A
but all implications on the left are members of w, so v(2A) 2A w, which implies
that v(w, 2A) v0 (w, 2A), contrary to assumption.
Now extend w00 to a maximal v(2A) A-consistent set, w0 . Then w0 T . Also, for
an arbitrary formula C, v0 (w, 2C) C w0 , and so v0 (w, 2C) v0 (w0 , C), and thus
wRw0 . Then:
V
v(w, 2A) =
{v(w0 , A) | wRw0 }
v(w0 , A)
= v0 (w0 , A)
But, by construction, v(w, 2A) A 6 w0 , so v(w, 2A) 6 v0 (w0 , A), a contradiction.
3) Now, the completeness proof is finished in the usual way. If an implication, X,
is not provable, is X-consistent. Extend it to a maximal X-consistent set, w. Then
w G, and it follows from the argument above that v(w, X) will not be true.
The proof above extends readily to allow nested implications, provided T has pseudocomplements, that is, provided T is distributive.

A Different Example

In the next section a system of modal logic is presented that allows models to have
many-valued accessibility relations. Before getting to the technical details, an example
is in order.
Suppose there are two experts, Rosencrantz and Guildenstern (R and G), who are
being asked to pass judgement on the truth of various statements, in various situations.
Then a natural truth-value space to work with is a four-valued one: neither says true; R
says true but G does not; G says true but R does not; and both say true. Truth values
can be identified with subsets of {R, G}. Now, two kinds of judgements are possible: 1)
A is true in situation w; and 2) w is a situation that should be considered. The first kind

of judgement can be thought of as assigning a truth value to A at the possible world

w. The second kind of judgement amounts to a many-valued accessibility relation.
Suppose, for instance, that there are three situations; this world, and two others,
w1 and w2 . Suppose both R and G say w1 should be considered, but only R says w2
should be. Suppose also that only G says A would be true in situation w1 , and nobody
says A would be true in situation w2 . The question is, how should A is true no matter
what, that is, 2A, be evaluated in this world?
It seems clear that the value of 2A in this world should be the meet of values
calculated for each accessible world; in a sense, it should be what is common to all
alternative situations. As far as w1 goes, everybody says it should be considered, but
only G says A is true there. Intuitively, from R we get a no, and from G a yes, as far as
the world w1 is concerned. Thus w1 contributes {G}. For w2 , G does not say it should
be considered at all. Then for G it can not serve as a counter-example, so in effect w2
counts as a yes for G. For R, on the other hand, w2 should be considered, but A is
false there, so w2 counts as a no for R. Thus w2 also contributes {G}, and so 2A in
this world should be given the value {G}.
On closer examination, the informal evaluation above really amounts to using the
following rule. The truth value of 2A is the intersection, over all worlds, of the truth
value of A at an alternative world union the complement of the accessibility value of
that alternative world. If we write R(w, w0 ) for the truth value of the accessibility
relation, R(w, w0 ) for its complement, and v(w, A) for the truth value of A at w, the
rule amounts to this.
v(w, 2A) =

{R(w, w0 ) v(w0 , A) | all w0 }.

To place this in context, note that the truth-value space above is a powerset algebra,
and hence is distributive. Distributive finite lattices have relative pseudo-complement
operations. Further, a natural notion of negation can be defined in any pseudo-boolean
algebra: a = (a false). In this case it is easy to check that the negation operation
is the same as set-theoretic complementation. Finally, it is a standard result about
pseudo-boolean algebras that when negation meets the condition that a a = true is
an identity, then a b = a b, [9]. Consequently, the evaluation rule given above is
equivalent to the following:
v(w, 2A) =

{R(w, w0 ) v(w0 , A) | all w0 }.

Finally it is this that is taken as definitive in what follows.

10

Many-valued modal logic, version II

For this section, assume T is a finite distributive lattice (hence with a relative pseudocomplement operation), and the language is L[2, ], allowing nested implications.
Definition 10.1 An implicational modal model is a structure hG, R, vi where G is a
non-empty set of possible worlds, R is a mapping from G G to T , and v maps worlds
and atomic formulas to T , again subject to the usual condition that members of T map
to themselves.

The mapping R can be thought of as a many-valued relation between possible worlds.

The mapping v is extended to all formulas as usual, with the following special condition:
v(w, 2A) =

{R(w, w0 ) v(w0 , A) | w0 G}

It is straightforward to verify that if R only takes on the values true and false, an
implicational modal model can be identified with a binary modal model in the obvious
way. It follows that any sequent that is valid in all implicational modal models is
also valid in all binary ones. The converse is not true, at least for sequents involving
constants. For instance, if c T is different from true or false, the sequent true
2c, 2c c will be valid in all binary modal models, but examples can be produced to
show it is not valid in all implicational ones.
The next job is to modify the basic Gentzen system to reflect validity in implicational
models. For this purpose, in place of the Binary Necessitation Rule, use the following.
Implicational Necessitation Rule For a1 , . . . , an , b T , and formulas A1 , . . . , An ,
B:
(a1 A1 . . . an An ) (b B)
(a1 2A1 . . . an 2An ) (b 2B)
The number n is allowed to be 0, in which case the rule is taken as
bB
b 2B
Notice that Theorem 7.5 says Implicational Necessitation is a derived rule in the system
allowing the Binary Necessitation Rule.
Soundness of the Implicational Necessitation Rule, with respect to implicational
modal models, is most easily shown indirectly. It is an easy consequence of the following.
Proposition 10.2 The following are sound rules, or valid sequents, with respect to
implicational modal models.
AB
1. 2A 2B
2. for each a T , 2(a A) (a 2A)
3. for each a T , (a 2A) 2(a A)
4. (2A 2B) 2(A B)
Proof We show two of the items simultaneously, the other two are straightforward.
The following makes use of fundamental properties of relative pseudo-complements, see
[9]. Let a T ; then:
v(w, 2(a A)) =
=
=
=
=
=
=

V
{R(w, w0 ) v(w0 , a A) | w0 G}
V
{R(w, w0 ) (v(w0 , a) v(w0 , A)) | w0 G}
V
{v(w0 , a) (R(w, w0 ) v(w0 , A)) | w0 G}
V
{a (R(w, w0 ) v(w0 , A)) | w0 G}
V
0
0
0

a {R(w, w ) v(w , A) | w G}
v(w, a) v(w, 2A)
v(w, a 2A)

Completeness is more work, naturally. Only the basic ideas will be sketched here
much detail is omitted. First, a somewhat different notion of consistency is needed.
The following definition is suitable for this section, and replaces the earlier notion of
consistency.
Definition 10.3 A set S is X-inconsistent if, for some finite {Y1 , . . . , Yn } S, the
sequent (Y1 . . . Yn ) X is provable. S is X-consistent if it is not X-inconsistent.
A set S that is X-consistent can be extended to a maximal one, S 0 , and it will be
the case that, for each for each formula Z there will be exactly one member t T such
that Z t and t Z are both in S 0 . The proof of this is via a reduction to Theorem 4.1
but is omitted here since it is both technical and simple.
Theorem 10.4 The modal system with the Implicational Necessitation Rule is complete
with respect to implicational modal models.
Proof Again take G to be the collection of all maximal X-consistent sets, for all X
(but with the notion of consistency as defined for this section). For w G, set v0 (w, A)
to be the unique a T such that A a and a A are both in w. And for w, w0 G,
V
set R(w, w0 ) = {v0 (w, 2A) v0 (w0 , A) | all formulas A}. Finally, set v to be the
same as v0 on atomic formulas. This determines an implicational modal model.
Following the usual style of completeness proof, the heart of the argument is to show
that v and v0 agree on all formulas. Once this is shown, the remaining parts are routine.
It is this part alone that is presented here. And in fact, only one case is considered,
that of necessitation.
Assume that, for some formula A, and for all worlds w G, v(w, A) = v0 (w, A). We
show v(w, 2A) = v0 (w, 2A).
First, by definition, R(w, w0 ) v0 (w, 2A) v0 (w0 , A). It follows by standard
properties of relative pseudo-complements that v0 (w, 2A) R(w, w0 ) v0 (w0 , A). So
V

v(w, 2A) =
{R(w, w0 ) v(w0 , A) | w0 G}
V
=
{R(w, w0 ) v0 (w0 , A) | w0 G}
v0 (w, 2A)
That is, v0 (w, 2A) v(w, 2A). Now suppose v(w, 2A) 6 v0 (w, 2A); we derive a
contradiction.
Let w0 = {v0 (w, 2B) B | all formulas B}. The claim is, w0 is v(w, 2A) Aconsistent. For if not, there are formulas B1 , . . . , Bn such that
[(v0 (w, 2B1 ) B1 ) . . . (v0 (w, 2Bn ) Bn )] [v(w, 2A) A]
but then by the Implicational Necessitation Rule,
[(v0 (w, 2B1 ) 2B1 ) . . . (v0 (w, 2Bn ) 2Bn )] [v(w, 2A) 2A]
But each implication in the hypothesis part is in w, and it follows that v(w, 2A)
2A w. But this implies that v(w, 2A) v0 (w, 2A), contradicting the assumption.
Thus w0 is v(w, 2A) A-consistent.
Extend w0 to w00 , maximal v(w, 2A) A-consistent. Now, v0 (w, 2B) B is
in w00 for each B, so v0 (w, 2B) v0 (w00 , B), and hence by standard properties of

relative pseudo-complement, v0 (w, 2B) v0 (w00 , B) = true. Since B is arbitrary,

R(w, w00 ) = true.
Further, v(w, 2A) A is not in w00 , so v(w, 2A) 6 v0 (w00 , A). But,
V

{R(w, w0 ) v(w0 , A) | w0 G}
v(w, 2A) =
R(w, w00 ) v(w00 , A)
= R(w, w00 ) v0 (w00 , A)
= v0 (w00 , A)
and this is a contradiction.
We have shown that v(w, 2A) v0 (w, 2A), and so v(w, 2A) = v0 (w, 2A).

11

Conclusion

The material presented in this paper is only a beginning on what is really needed.
The most glaring omission is that not enough intuitive feeling for these logics has been
presented. What are their distinguishing characteristics? How do they differ from each
other? Frankly, I wish I could say more about this. Investigation of many-valued modal
logics, especially allowing many-valued accessibility, is at an early stage, and answers
to important questions like these must wait on more experience. I invite others to
investigate here.
All the logics considered above are analogs of the modal logic K. No special conditions are placed on the accessibility relations. For the binary version, conditions like
transitivity, reflexivity, and so on, are straightforward. For the version allowing accessibility to be many-valued, though, analogs of these conditions are available. For
instance, a requirement that R(w, w0 ) R(w0 , w00 ) R(w, w00 ) is a natural generalization of transitivity. I do not know what effect imposing conditions like these will have.
Work remains here too.
Finally the proof procedures given above, though based on Gentzen systems, are far
from automatable. It seems clear that the Cut Rule is not eliminable, for instance. Still,
automatable many-valued proof procedures based on different principles are possible,
see [2, 3]. I have made some progress on extending these notions to the modal case,
but presentation of the results must wait on further research.

Appendix
In this appendix are presented the results needed to establish completeness of the nonmodal many-valued sequent calculus (Section 4). The material is divided into two
sections, the first containing general lattice-theoretic results, the second a derived rule
of the sequent calculus.

12

Spanning sets

Completeness will follow primarily from a derived rule given in the next section. Since
all that is being assumed about T is that it is a finite lattice, some way is needed
for grouping members so that results about T can be proved uniformly. That is the
purpose of this section. First, some convenient general terminology.

Definition 12.1 For A, B T , A B means: for every a A there is some b B

with a b, and for every b B there is some a A with a b. (This is sometimes
called the Egli-Milnor ordering.) The notation A < B means A B but not B A.
It is easy to check that this gives a transitive relation on subsets of T , but not an
antisymmetric one. Also {false} is smallest in this relation, and {true} is biggest.
Definition 12.2 Two members a, b T are comparable if a b or b a; a and b
are incomparable if they are not comparable. A set A T is an antichain if any two
distinct members are incomparable.
It is straightforward to prove that, if A and B are antichains and A B and B A,
then A = B. Thus on antichains of T we have a partial ordering.
Definition 12.3 A set A T is a spanning set if A is an antichain and every member
of T is comparable with some member of A.
There are many spanning sets. The sets {false} and {true} are spanning sets.
Also, any maximal antichain (maximal under the subset relation) is a spanning set.
Consequently, every antichain can be extended to a spanning set.
Definition 12.4 If A T is a spanning set, b is below A if b a for some a A, and
b is above A if a b for some a A. Likewise, b is strictly below A if b is below A but
b 6 A; similarly for strictly above.
For a spanning set A, by the comparability condition, every member of T is either
above or below A. And it follows from the independence condition that if a member of
T is both above and below A, it is in A. Thus, for each a T , exactly one of: a is in
A, a is strictly above A, a is strictly below A.
Proposition 12.5 Suppose A and B are spanning sets in T with A B. And suppose
some member of T is strictly above A and strictly below B. Then there is a spanning
set C such that A < C < B.
Proof A member of T that is strictly above A and strictly below B will be referred
to as being strictly between A and B. Now, construct a set C in stages, as follows. Let
C0 be a maximal antichain in T whose members are strictly between A and B. By
hypothesis, C0 is not empty. Next, extend C0 by adding members of A, one at a time,
in any order, until no more can be added while preserving the antichain property; call
the resulting set C1 . Finally, extend C1 by adding members of B, again until no more
can be added while preserving the antichain property. Call the resulting set C.
By construction, C is an antichain. Every member of T is comparable with C, by
the following argument. Suppose x T . By remarks above, if x is not strictly between
A and B, x must be below A or above B. Consequently the argument divides into three
parts.
1) Suppose x is strictly between A and B. If x is in C0 we are done. If not, it must
be comparable with some member of C0 , since C0 was a maximal antichain in T . Either
way, x is comparable with C.
2) Suppose x is below A. Then x a for some a A. If a C1 , x is below C1
and hence below C. If a 6 C1 , adding it would yield a set that is not an antichain.

Since members of A are incomparable, it must be that a and c are comparable for some
c C0 . If a c then x c, and hence x is below C. If c a a contradiction can be
derived, as follows. Since c is strictly above A, a0 c for some a0 A. Then a0 a,
and from the fact that A is an antichain it follows that a0 = a. Then c = a A,
contradicting the fact that c is strictly above A.
3) Finally, suppose x is above B. Then b x for some b B. If b C, x is above
C and we are done. If b 6 C, b is comparable with some member of C. Since B is an
antichain, b must be comparable with some member of C1 . Now the case divides in two.
3a) Suppose b is comparable with some member c of C0 . If c b then c x, so x is
above C. The alternative, b c, is impossible, by an argument similar to that given in
case 2).
3b) Suppose b is comparable with some member c of C1 C0 . If c b then c x
so again x is above C. Now suppose b c. Since c C1 C0 , c A, and since A B,
for some b0 B we have c b0 . Then b c b0 , and since B is an antichain, it follows
that b = c = b0 . Since b x, c x, so x is above C in this case also.
Finally it must be shown that A < C < B. An argument to establish that A C B
is along lines similar to that above. If C A, then we would have A = C, which is
impossible since C contains members strictly above A. Thus A < C. Similarly C < B.
Now, suppose B is a spanning set, and B 6= {false}. Then there are spanning sets
< B, in particular, {false}. Since T is finite, there must be some spanning set A < B
that is maximal (in the ordering) among spanning sets that are < B; such an A is
said to be immediately beneath B. By Proposition 12.5, if A is immediately beneath B,
there can be no members of T strictly between A and B. Thus the following has been
established, a result which plays a fundamental role in the next section.
Proposition 12.6 If B is a spanning set different from {false}, there is a spanning set
A immediately beneath B and, for every x T , either x is below A or x is above B.

13

A Fundamental derived rule

This section is devoted to the statement and proof of a derived rule that plays a basic
role in the completeness proof of Section 4. The first item is a Lemma about spanning
sets, amounting to a formalized version of part of Proposition 12.6.
Lemma 13.1 Suppose A = {a1 , a2 , . . . , an } and B = {b1 , b2 , . . . , bk } are two spanning
sets in T , with A immediately beneath B. Then the following sequent is provable, for
any formula A:
A a1 , . . . , A an , b1 A, . . . , bk A.
Proof It is simplest to present the proof backwards. We want to prove
A a1 , . . . , A an , b1 A, . . . , bk A.
Using Rule RI , this would follow if we could show, for every c1 T ,
c1 A c1 a1 , A a1 , . . . , A an , b1 A, . . . , bk A.

If c1 is above B, then for some i, bi c1 , and then bi c1 . But bi c1 , c1 A

bi A, from which the desired sequent is obtained by Cut and Thinning. Thus it
remains to show the sequent for c1 not above B, which implies that c1 is below A. If
c1 a1 we easily get the sequent by Thinning, from c1 a1 . We are still left with
the remaining cases. To summarize: we are done if we can show
c1 A c1 a1 , A a1 , . . . , A an , b1 A, . . . , bk A
under the assumption that c1 is below A but c1 6 a1 .
The same argument can be repeated using Rule RI with each of A a2 , . . . ,
A an . This reduces the problem to showing:
c1 A, . . . , cn A c1 a1 , . . . , cn an , A a1 , . . . , A an , b1 A, . . . , bk A
where each of c1 , . . . , cn is below A, but for each i, ci 6 ai .
Next, a similar procedure can be applied to each of b1 A, . . . , bk A, this time
using Rule RI, reducing the problem to showing:
c1 A, . . . , cn A, A d1 , . . . , A dk c1 a1 , . . . , cn an ,
b1 d1 , . . . , bk dk ,
A a1 , . . . , A an ,
b1 A, . . . , bk A
where each of c1 , . . . , cn is below A, but for each i, ci 6 ai , and each of d1 , . . . , dk
is above B, but for each j, bj 6 dj . In fact, this will be established by showing that,
under these restrictions on ci and dj ,
c1 A, . . . , cn A, A d1 , . . . , A dk .
Note that, using Conjunction and Disjunction Axioms,
c1 A, . . . , cn A, A d1 , . . . , A dk c1 . . . cn d1 . . . dk
so it is enough to prove
c1 . . . cn d1 . . . dk
and by a Propositional Constant Axiom, this will follow provided
c1 . . . cn 6 d1 . . . dk
so it is this, finally, that must be established.
Suppose c1 . . . cn were below A. Then, for some i, c1 . . . cn ai . But then,
ci ai , contrary to the conditions above. Consequently c1 . . . cn is not below A so,
by Proposition 12.6, c1 . . . cn must be above B. Then bj c1 . . . cn for some j.
Now, if we had c1 . . . cn d1 . . . dk , it would follow that bj dj , again contrary
to the conditions above. Consequently we do not have c1 . . . cn d1 . . . dk , which
concludes the proof.
Now it is possible to prove Theorem 4.1, which is restated here for convenience.
Theorem 4.1 The following is a derived rule:
, A t, t A (for all t T )

Proof Assume, for the rest of this proof, that , A t, t A is provable, for
each t T . It will be shown that also has a proof. Spanning sets are the chief
tool here.
For this proof only, call a spanning set A good if , a A has a proof, for each
a A.
Using the partial ordering, , on spanning sets, defined in Section 12, the biggest
spanning set is {true}. It is good, a fact that follows from our hypothesis, and from
Proposition 3.5 as follows:
, A true, true A A true
Cut
, true A
Next, suppose B = {b1 , b2 , . . . , bk } is a good spanning set, and A = {a1 , a2 , . . . , an }
is a spanning set that is immediately beneath B. Then A is also good, by the following
argument. First, by Lemma 13.1 the following sequent is provable:
A a1 , . . . , A an , b1 A, . . . , bk A.
Since B is good, for each j = 1, 2, . . . , k the following sequent is provable:
, bj A .
Then k applications of Cut yield:
, A a1 , . . . , A an .
Next, using the proof hypothesis,
, A a1 , a1 A , A a1 , . . . , A an
Cut
, a1 A , A a2 , . . . , A an
Also members of A are incomparable, so we have the following:
a1 A, A a2 a1 a2 a1 a2
Cut
a1 A, A a2
Combining these,
, a1 A , A a2 , . . . , A an a1 A, A a2
Cut
, a1 A , A a3 , . . . , A an
Proceeding in this way, each of a3 , . . . , an can be eliminated, thus establishing the
provability of:
, a1 A .
But the choice of a1 was arbitrary. A similar argument shows the provability, for each
i = 1, 2, . . . , n of
, ai A
and thus A is good.
Now, start with {true}. Choose a spanning set immediately beneath it, one immediately beneath that, and so on. In this way a descending sequence of spanning sets
is produced. But since T is finite, such a sequence must terminate; a spanning set

must be reached with no other immediately beneath it. By Proposition 12.6, the only
such spanning set is {false}, so this is where the sequence terminates. Now, the first
member, {true}, of the sequence is good, as was shown earlier. Then each member of
the sequence must be good, by the argument above, and so {false} must be good, and
thus , false A is provable. This, combined with Proposition 3.5, concludes the
argument.
, false A false A
Cut

References
[1] Stephen Blamey. Handbook of Philosophical Logic, volume 3, chapter Partial Logic,
pages 170. D. Reidel Publishing Company, 1985.
[2] R. J. Hahnle. Towards an efficient tableau proof procedure for multiple-valued logics. In Proceedings Workshop Computer Science Logic, Heidelberg, Lecture Notes
on Computer Science. Springer-Verlag, 1990.
[3] R. J. Hahnle. Uniform notation of tableau rules for multiple-valued logics. In
Proc. Twenty-First Intl. Symp. on Multiple-Valued Logic, pages 238245. IEEE
Computer Society Press, 1991.
[4] Stephen C. Kleene. Introduction to Metamathematics. D. Van Nostrand, Princeton, NJ, 1950.
[5] Saul Kripke. Outline of a theory of truth. The Journal of Philosophy, 72:690716,
1975. Reprinted in New Essays on Truth and the Liar Paradox, R. L. Martin, ed.,
Oxford (1983).
[6] Charles G. Morgan. Local and global operators and many-valued modal logics.
Notre Dame Journal of Formal Logic, 20:401411, 1979.
[7] Osamu Morikawa. Some modal logics based on a three-valued logic. Notre Dame
Journal of Formal Logic, 30:130137, 1989.
[8] Pascal Ostermann. Many-valued modal propositional calculi. Zeitschrift f
ur mathematische Logik und Gr
undlagen der Mathematik, 34:343354, 1988.
[9] Helena Rasiowa and Roman Sikorski. The Mathematics of Metamathematics.
PWN Polish Scientific Publishers, Warsaw, third edition, 1970.
[10] J. B. Rosser and A. R. Turquette. Many-valued Logics. North-Holland Publishing
Company, Amsterdam, 1952.
[11] Peter K. Schotch, Jorgen B. Jensen, Peter F. Larsen, and Edwin J. MacLellan. A
note on three-valued modal logic. Notre Dame Journal of Formal Logic, 19:6368,
1978.
[12] Krister Segerberg. Some modal logics based on a three-valued logic. Theoria,
33:5371, 1967.

[13] S. K. Thomason. Possible worlds and many truth values. Studia Logica, 37:195
204, 1978.

Research supported by NSF Grant CCR-8901489.