# * Operational Modal Logic *

## by Sergei Artemov

1995-1996

This work is closely related to our previous study of reflection in type theory. The modal logic he has in mind is Godel's system S4, a logic of provability. Sergei has a new axiomatization which uses "proof expressions" and is related to propositions-as-types. He shows the logic complete in two senses which he will explain.