Bringing it about (Q910393)

In this very nice article the author presents a logic of ``bringing it about that A'' or simply ``doing A'' in the sense that the truth of the assertion A is established. The logic is an extension of propositional dynamic logic (PDL) without program letters but with expressions of type \(\delta\) A (``doing A'') as atomic programs. The typical axioms with respect to \(\delta\) A are [\(\delta\) A]A (doing A establishes A) and [\(\delta\) A]B\(\supset ([\delta B]C\supset [\delta A]C)\) (a form of transitivity with respect to establishing). A semantical model is given, the essence of which is the interpretation of \(\delta\) A as the input/output relation of a program that establishes A at/as its output. Finally, an almost self-contained proof is provided of the soundness and completeness of the logic with respect to the model. Although motivated from a philosophical point of view, I believe the logic is also of interest to AI researchers and computer scientists involved in program/system specification.