The main purpose of the paper is to introduce philosophers and philosophical logicians to dynamic logic, a subject which promises to be of interest also to philosophy. A new completeness result involving both after — and during — operators is announced.

We consider a quantifier-free language in which there are terms as well as formulas. The proposition-forming propositional operators are the usual ones, and the term-making term operators are the usual lattice theoretical ones. In addition there is a formula-making term operator, does. We study a new logic in which does is claimed to approximate some features of the informal concept the agent performs the action.