| We develop two independent extensions of normal modal logic following the ideas proposed by McCarthy in his writings on "context." The first is: in a deductive system, to treat modalities as assumptions, just like formulas. This enables us to define a calculus for normal modal logic which allows for the deduction theorem. The second idea is to treat modalities as objects of first-order theories. We provide semantics and a complete calculus. |