Litak, Visser, “Lewis meets Brouwer: constructive strict implication”
It is known that monadic and comonadic calculi correspond via Curry-Howard to modal logics with a unary modality □, but what about Hughes’ arrows? It turns out that they correspond to a binary modality ⥽ - the so-called “strict implication”. Moreover, Lewis’s original formulation of modal logic introduced strict implication as a primary construct, and □ was expressed using it. After a series of works by Gödel, the arrow was forgotten in favor of the box, also because in the classical version these modalities are mutually expressible. As usual, in the constructive formulation, symmetry breaks up into independent entities with different semantics - by adding additional schemes to strict implications, one can obtain a logic for arrows or guarded recursion.