Not all objects will typically exist in all contexts. To deal with this phenomena, we introduce existence as a predicate, . Intuitively,
is true iff the object denoted by x exists in the context denoted by c.
If the domains of all the contexts are not the same, then formulas 60--63 are not intuitively correct. Instead, a domain precondition needs to be added to all the formulas. For example instead of formula 61, we would write
The main implication connective in this formula might not be classical (see [12]).
Note however, if we simply change the abbreviation of to
then the axioms involving (axioms 40-42 and 58-59) will still be true. In other words, the previous domain formalizations remain unaltered. To verify this, note that substituting this new definition for value (given in formula 65) into formula 40 gives us formula 64, rather then formula 61.
We also need to assert that the problem solving context contains all the objects present in the other contexts which are involved in the particular problem solving process. In some outer context c0 we would write:
In both cases mentioned above, the rules of entering and exiting a context for the function will follow from the general rules enter and exit for the .
This approach is similar to the treatment of existence in quantificational modal logics which are based on free logics; see [55]. Many of the philosophical issues involved in quantifying across worlds with different domains apply also here; see [36] for discussion. For example, it is well known from quantificational modal logic that the classical rule of universal instantiation is not valid for non-rigid terms. Logics of context which allow functions, will thus need to have a restricted form of universal instantiation.