Typesetting modal logic

Modal logic extends propositional logic with two new operators, a- ("box") and a- ("diamond"). There are many interpretations of these two symbols, the most common being necessity and possibility respectively. That is, a-p means the proposition p is necessary, and a-p means that p is possible. Another interpretation is using the symbols to represent things a person knows to be true and things that may be true as far as that person knows.

There are also many axiom systems for inference concerning these operators. For example, some axiom systems include the rule

and some do not. If you interpret a- as saying a proposition is provable, this axiom says whatever is provable is provably provable, which makes sense. But if you take a- to be a statement about what an agent knows, you may not want to say that if an agent knows something, it knows that it knows it.

See the next post for an example of applying logic to security, a logic with lots of modal operators and axioms. But for now, we'll focus on how to typeset the box and diamond operators.

LaTeX

In LaTeX, the most obvious commands would be \box and \diamond, but that doesn't work. There is no \box command, though there is a \square command. And although there is a \diamond command, it produces a symbol much smaller than \square and so the two look odd together. The two operators are dual in the sense that

and so they should have symbols of similar size. A better approach is to use \Box and \Diamond. Those were used in the displayed equations above.

Unicode

There are many box-like and diamond-like symbols in Unicode. It seems reasonable to use U+25A1 for box and U+25C7 for diamond. I don't know of any more semantically appropriate characters. There are no Unicode characters with "modal" in their name, for example.

HTML

You can always insert Unicode characters into HTML by using &#x, followed by the hexadecimal value of the codepoint, followed by a semicolon. For example, I typed □ and ◇ to enter the box and diamond symbols above.

If you want to stick to HTML entities because they're easier to remember, you're mostly out of luck. There is no HTML entity for the box operator. There is an entity ◊ for "lozenge," the typographical term for a diamond. This HTML entity corresponds to U+25CA and is smaller than U+25c7 recommended above. As discussed in the context of LaTeX, you want the box and diamond operators to have a similar size.

Related posts

• Intuitionistic logic in Gilbert and Sullivan
• Math symbols in HTML, TeX, and Unicode
• Modal logic systems S1-S5
• Modal and temporal logic for security