Catalogue of Artificial Intelligence Techniques
Keywords: possible worlds, rule of necessitation
Categories: Inference and Reasoning , Logic Programming
Author(s): Colin Phillips
True propositions can be divided into those--such as `2+2=4'--which are necessarily true and those--such as `Mars has two moons'--which are contingently true. If ` ' is some proposition then we write ` ' (or ) to mean ` is necessarily true'. We can define ` ' (or ), read as ` is possibly true', as equivalent to ` '. ` ' and ` ' are modal operators. A modal logic is an extension of standard logic obtained by adding to some the modal operators together with appropriate axioms and rules of inference. A great many systems of modal logic have been constructed of which the most important are systems T, S4 and S5. The modal system T has as axioms some set of axioms appropriate to the standard propositional calculus together with:
We add to the rules of inference of our standard logic a rule of necessitation to the effect that if is theorem then so is
. The system S4 is obtained by adding to T:
and S5 by adding to T:
Modal predicate logic can be obtained by making analogous additions to standard Predicate Logic. To construct a model of one of the above systems we postulate a set of possible worlds , an assignment of a truth value to each atomic formula for each world and a relation of accessibility between a particular world and a subset of . ` ' is true in a world in such a model if and only if it is true in every world accessible to that world in that model. A proposition is valid if and only if it is true in every such model. If we require that the accessibility relation be reflexive then the valid propositions are those provable in T. If we also require that the system be transitive then we get as valid the theorems of S4. Finally if we also require that the relation be symmetric we get as valid the theorems of S5.
- Hughes, G.E. and Cresswell, M.J., An Introduction to Modal Logic
, Methuen, London, 1972.