Constructive Modalities with Provability Smack

TL;DR

This paper reviews the Tbilisi school's work on intuitionistic modal logics related to well-founded and scattered structures, emphasizing fixed-point theorems and their implications for theoretical computer science.

Contribution

It synthesizes the development of intuitionistic modal logics with a focus on fixed-point theorems and their applications in computer science.

Findings

Connections between intuitionistic modal logics and well-founded structures

Implications of fixed-point theorems in logic and computer science

Overview of the Tbilisi school's contributions to the field

Abstract

I overview the work of the Tbilisi school on intuitionistic modal logics of well-founded/scattered structures and its connections with contemporary theoretical computer science. Fixed-point theorems and their consequences are of particular interest.