  Propositional term modal logic is interpreted over Kripke structures with
unboundedly many accessibility relations and hence the syntax admits variables
indexing modalities and quantification over them. This logic is undecidable,
and we consider a variable-free propositional bi-modal logic with implicit
quantification. Thus $[\forall] \alpha$ asserts necessity over all
accessibility relations and $[\exists] \alpha$ is classical necessity over some
accessibility relation. The logic is associated with a natural bisimulation
relation over models and we show that the logic is exactly the bisimulation
invariant fragment of a two sorted first order logic. The logic is easily seen
to be decidable and admits a complete axiomatization of valid formulas.
Moreover the decision procedure extends naturally to the `bundled fragment' of
full term modal logic.
