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.