Axioms in modal logic often say that one sequence of boxes and diamonds in front of a proposition *p* implies another sequence of boxes and diamonds in front of *p*. For example, Axiom 4 says

□ *p* → □□ *p*

and Axiom 5 says

◇*p* → □◇*p*.

Every axiom has a dual form. The dual form of Axiom 4 is

◇◇*p* → ◇*p*

and the dual of Axiom 5 is

◇□ *p* → □ *p*.

## Computing duals

There’s a simple way to compute the dual of such axioms:

**Rotate all the squares 45° and rotate the arrow 180°**.

This turns boxes into diamonds, diamonds into boxes, and flips the direction of implication.

## Shell and Perl

We could do this using the `tr`

utility at the command line

$ echo '□□◇□◇p → □◇p' | tr '□◇→' '◇□←' ◇◇□◇□p ← ◇□p

We could also do the same thing in Perl, using its `tr`

operator

$prop = "□□◇□◇p → □◇p"; ($dual = $prop) =~ tr/□◇→/◇□←/; print "$prop\n$dual\n";

This prints

□□◇□◇p → □◇p ◇◇□◇□p ← ◇□p

It’s important to note that `tr`

in both its incarnations does **simultaneous** replacement. It did what we expected, so it might be hard to notice.

`tr`

takes two strings of the same length as arguments. Call the first one *from* and the second *to*. The easiest way to implement `tr`

would have been to replace the first character of *from* with the first character of *to*, then replace the second character of *from* with the second character of *to*, etc.

This would have turned all our boxes into diamonds, then turned all diamonds into boxes, and so we’d be left with nothing but boxes! Our sequence □□◇□◇ would have turned into □□□□□.

## Proof

Why is the rule above valid?

Let ○ stand for either a box or a diamond and suppose we start with

○_{1} ○_{2} … ○_{m} *p* → ○_{m+1} ○_{m+2} … ○_{n} *p*

where *p* is an arbitrary proposition.

Now let ○’ stand for the dual of ○. So if ○ is a box, ○’ is a diamond, and vice versa. Then

○ *p* = ¬○’ ¬*p*

by definition. (If you take □ as primary, then the equation above is the definition of ◇. If you take ◇ as primary, it’s the definition of □.) Apply this rule everywhere.

¬○’_{1} ¬¬○’_{2} ¬… ¬○’_{m} ¬*p* → ¬○’_{m+1} ¬¬○’_{m+2} … ¬○’_{n} ¬*p*

Now cancel out all the pairs of consecutive negations.

¬○’_{1} ○’_{2} … ○’_{m} ¬*p* → ¬○’_{m+1} ○’_{m+2} … ○’_{n} ¬*p*

Now take the contrapositive: (¬*P* → ¬*Q*) → (*Q* → *P*).

○’_{m+1} ○’_{m+2} … ○’_{n} ¬*p* → ○’_{1} ○’_{2} … ○’_{m} ¬*p*

Since *p* was an arbitrary proposition, we can replace *p* with ¬*p*.

○’_{m+1} ○’_{m+2} … ○’_{n} *p* → ○’_{1} ○’_{2} … ○’_{m} *p*

What we have above is the proposition we started with, with all the boxes replaced with diamonds, all the diamonds replaced with boxes, and the direction of the implication reversed.

## More modalities

Notice that the theorem and proof still holds if there are multiple modalities. Suppose we have a set of modalities *K*_{i}. You could interpret

*K*_{i }*p*

as saying the *i*th agent knows proposition *p* is true. Then the dual is defined by

*K’*_{i }*p* = ¬ *K*_{i }*¬ p*,

which could be interpreted as saying the *i*th agent does not know *p* to be false.

You could form the dual of a proposition involving *K* and *K*‘ expressions by adding primes to terms that don’t have them, and removing primes from terms that do, and turning the implication around. The proof would be the same as above, only we don’t restrict ○ to being □ or ◇.

I suppose this does not work in an intuitionistic context wherein one cannot eliminate double negations willy-nilly?

Modal logic includes the law of the excluded middle, so it’s not intuitionistic.

However, it’s possible to embed intuitionistic logic in S4. More on that here.