Axiom S5
From Wikipedia, the free encyclopedia
Axiom S5 is the distinctive axiom of the S5 modal logic and says that if necessarily possibly p, then possibly p and if possibly necessarily p then necessarily p. There are some who make the claim that the latter description is faulty.
The S5 axiom is usually introduced to systems that already have Duality, and so this axiom is given as either
* Possibly P implies Necessarily Possibly p [] * Possibly Necessarily P implies Necessarily p [
]
which are equivalent in such systems. So both of these axioms are properly called axiom 5
Basic "Introduction to Modal Logic" books (for example Hughes and Cresswell's, or Brian Challas') show how this leads in S5 to theorems that can remove all but the last modal operator in a modal stack and get something equivalent to just the last one.
