Intuitionist predicate logic can be interpreted in quantified S4 by the
mapping *t* defined as
                t(p)    =       []p
                t(A & B)=   t(A) & t(B)
                t(A v B)=       t(A) v t(B)
                t(A –> B)=  [](t(A) –> t(B))
                t(-A)   =       []t(A)
                t(UxPx) =       [](Ux)t(Px)
                t(ExPx) =       (Ex)t(Px).

Question: in the usual Kripke-semantics for intuitionist predicate logic, the
domains must be nested, i.e., if *a* and *b* are two nodes and *Da* and *Db*
are the respective domains of these nodes, then if *aRb* (where *R* is the
usual partial-ordering), then *Da* is a subset of *Db*. Given the
interpretability of intuitionist predicate logic in quantified S4, does this
mean that the domains in a model for quantified S4 are nested? [In other words,
does quantified S4 really have any models in which the domains aren't nested?]

        The mapping *t* can be used to interpret classical predicate logic in
quantified S5. Does this mean that the domains in models for quantified S5 are
nested? [In other words, does quantified S5 have models in which the domains
aren't nested?]