The authors provide various propositional logics for the dynamic implication studied by Kamp, Groenendijk, Stokhof, and others to analyse some natural language phenomena. The underlying idea in these theories, which analyses sentence meanings as active entities transforming state spaces like computer programs, is abstracted in the framework of two-dimensional propositional modal logic so that the dynamic implication is characterized as a binary modal operator by a sort of two-dimensional Kripke models, which are called square models. The binary modality thus characterized, is then reinterpreted in the context of Boolean modal logic of Gargov et al. and axiomatised in Hilbert style on classical propositional logic. The Boolean-connective-free fragment of such logics is also examined and formulated in a tableau system featuring Fitting's prefixed formula method.