Sound substitution into modal contexts

Abstract

I review the problems involved in substituting into modal contexts, and state a rule which permits this to be done soundly. Such a rule justifies a expanded substitution process for modal logic. The process is syntactic but incurs proof obligations. I show constructs that permit the naming of objects outside the current modal contexts. These devices were motivated by problems found while using modal logic in planning.