We consider an extension of the propositional modal logic S4 which allows ◇ to act not only on isolated formulas, but also on sets of formulas. The interpretation of ◇Γ is then given by the tangled closure of the valuations of formulas in Γ, which over finite transitive, reflexive models indicates the existence of a cluster satisfying Γ. This extension has been shown to be more expressive than the basic modal language: for example, it is equivalent to the bisimulation-invariant fragment of FOL over finite S4 models, whereas the basic modal language is weaker. However, previous analyses of this logic have been entirely semantic, and no proof system was available. In this paper we present a sound proof system for the polyadic S4 and prove that it is complete. The axiomatization is fairly standard, adding only the fixpoint axioms of the tangled closure to the usual S4 axioms. The proof proceeds by explicitly constructing a finite model from a consistent set of formulas.
展开▼
