Axiom S5
From Wikipedia, the free encyclopedia
Axiom S5 is the distinctive axiom of the S5 system of modal logic and says that if possibly necessarily p, then necessarily p. (Or, equivalently: if possibly p then necessarily possibly p.)
Axiom S5 is at the heart of Plantinga's ontological argument. If the modality here is what Alvin Plantinga calls "broadly logical" necessity and possibility, then an argument for the axiom can be given as follows:
- If possibly necessarily p, then there is a possible world w at which p necessarily holds,
- Then, it is true at w that p is a broadly logically necessary truth, something whose negation would in a broadly logical sense be self-contradictory,
- But if something is self-contradictory at some possible world, then it is self-contradictory at all worlds,
and Plantinga holds that this is true even in the case of broadly logical self-contradictions as well.
In terms of Kripke semantics, S5 describes sets of possible worlds on which the accessibility relation is symmetric, transitive, and reflexive--that is, an equivalence relation. Roughly, any worlds among which any chain of accessibility relations holds, are themselves accessible to one another.
Axiom S5 can be seen to be true on any such model as follows:
- Suppose that Possibly, necessarily p is true at w0,
- Then there is some w1 such that Necessarily p is true at w1,
- In that case, p is true at every world., including a fortiori every world accessible from w0.
So Necessarily, p is true at w0.