[FOM] Modal logic with scope-modifying operators

[Aatu Koskensilta]

A few years ago I thought of an obvious extension of modal predicate 
logic in which subformulae of a modally quantified formula may be 
"exempted" from the scope of the modal operator (looking "backwards") 
and subformulae of such exempted formulae may again be introduced into 
the scope (looking "forwards"). This is achieved by adding two 
operators \ and /. The semantics for this extension can be given in a 
natural fashion by defining the relation "the sequence of worlds 
w_1,...,w_n at indek k satisfies the formula P" so that

  i. when \ is encountered, the index is decreased
  ii. when / is encountered, the index is increased
  iii. when [] is encountered, the sequence of worlds is cut at indek k, 
and all
       sequences w_1,...,w_k,w' are evaluated with the formula in scope 
of []

and saying that P is true at world w if "the sequence of worlds w at 
index 1 satisfies the formula P".

(There are restrictions on the appearance of \ and / so that evaluating 
the truth value of a well-formed formula never leads to a negative 
index or an index exceeding the length of the sequence of worlds 
w_1,...,w_n. Also, some notion of trans-world identity is needed, but 
here we can just assume that an individual x in a world w is identical 
to an individual y in world w' just in case x=y. Something must also be 
done about the interpretation of such formulae as P(x,y) when x and y 
come from different worlds, but here it does not matter if we just 
always consider such formulae false.)

In the propositional case nothing is gained in expressiveness. But in 
case of modal predicate logic when we consider the frame which contains 
all first order models of the signature in question it turns out that 
the expressive power is enormous (provided the vocabulary is 
sufficiently rich, ie. does not consist solely of monadic predicates). 
We can formulate such sentences as "necessarily in any world in which 
the actual individuals exist and in addition such-and-such predicates 
satisfy the axioms of ZFC with the actual individuals as ur-elements, 
such and such holds" and "for any possible world there exists an actual 
individual A such that the actual individuals existing in the possible 
world bear the relation \in to A, provided there is an actual 
individual such that all the individuals in the possible world bear 
relation \in to it" (comprehension axiom). This can be continued to 
tedious and ludicurous lengths.

This being such an obvious extension of modal predicate logic, it must 
surely have been studied previously. I'd be grateful for any 
references. In particular I'd like to know whether anything interesting 
can be done if the accessibility relation is restricted in some 
interesting fashion (i.e. not all first order models (worlds) of the 
given signature are accessible from any given model (world)).

Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus