# [FOM] Modal logic with scope-modifying operators

Aatu Koskensilta aatu.koskensilta at xortec.fi
Tue Dec 27 06:02:17 EST 2005

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