Bi-Heyting algebras, toposes and modalities (Q1914371)

A new approach to the modal operators of necessity and possibility is presented. This approach is based on the existence of two negations \((\neg\) and \(\sim)\) in bi-Heyting algebras. The modal operators \(\square\) and \(\diamondsuit\) are defined in bi-Heyting algebras by iterating certain combinations of these negations and going to the limit in the following way: \(\square_0 = \diamondsuit_0 = \text{Id}\), \(\square_{n + 1} = \neg \sim \square_n \), \(\diamondsuit_{n + 1} = \sim \neg \diamondsuit_n\), and \(\square a = \bigwedge_n \square_n a\), \(\diamondsuit a = \bigvee_n \diamondsuit_n a\). The authors study the properties of these operators and they apply them to define modal operators on the lattice of subobjects of a topos. Significant examples are given by means of graphs.