Skip to main content
PRL Project

Operational Modal Logic

by Sergei Artemov

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.