Systems like
T and S5 can be determined by specifying
certain rules of inference (which
in both cases include the rules
of first-order logic)
and axiom-schemata. The key axiom-schema
in T is the one known by that name, viz., 6#6;
the key axiom-schema in S5 is 5: 7#7.
(S5 includes as a theorem the
interesting 8#8, which becomes
relevant later in the paper.) In both systems, moving a negation sign
through a modal operator changes that operator (from diamond to box, and
vice versa) in a manner perfectly analogous to the rule of quantifier
negation in first-order logic.
For a succinct
presentation of the core ideas behind (propositional)
S5 see Chapter 1 of [1] (a book which includes discussion
of T and other systems as well).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.