Actuality in Intuitionistic Logic

In "Empirical Negation", Michael De takes up the challenge of extending intuitionism from mathematical discourse to empirical discourse, and to this end, he introduced an expansion of intuitionistic propositional logic obtained by adding a unary connective called empirical negation. The intuitive reading of empirical negation of A is: it is not the case that there is sufficient evidence at present that A. From a model-theoretic perspective, cashed out in terms of pointed Kripke models for intuitionistic logic, empirical negation of A is forced at a point iff A is not forced at the base point. Then, a simple calculation reveals that double empirical negation of A is forced at a point iff A is forced at the base point. In other words, double empirical negation can be seen as an actuality operator explored by John N. Crossley, Lloyd Humberstone, Martin Davies and more. Based on these, we introduce an expansion of intuitionistic propositional logic obtained by adding actuality. Our main results include sound and strongly complete axiomatization as well as comparisons to closely related systems such as Global Intuitionistic Logic of Satoko Titani as well as LGP of Matthias Baaz.