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. In traditional Logic, an axiom or postulate is a proposition that is not proved or demonstrated but considered to be either self-evident, or subject In Logic and Philosophy, S5 is one of five systems of Modal logic proposed by Clarence Irving Lewis and Cooper Harold Langford in 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 [$\Diamond p \to \Box\Diamond p$]  * Possibly Necessarily P implies Necessarily p [$\Diamond\Box p \to \Box 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.