PRL Seminars
Operational Modal Logic
Sergei Artemov
Visitor from Moscow State University and the Steklov Institute
January 29, 1996
Visitor from Moscow State University and the Steklov Institute
January 29, 1996
Abstract
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.