Skip to main content
PRL Project

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.