Algebraic axiomatization of tense intuitionistic logic (Q657427)

The paper studies the tense intuitionistic logics. The algebraic models of such logics are Heyting algebras endowed with tense operators. The operators \(G\) (it is always going to be the case that) and \(H\) (it has always been the case that) can be defined by the following conditions: 1. \(G(1) = 1\) and \(H(1) = 1\); 2. \(G(x \to y) \leq G(x) \to G(y)\) and \(H(x \to y) \leq H(x) \to H(y)\); 3. \(G(x \land y) \leq G(x) \to G(y)\) and \(H(x \land y) \leq H(x) \to H(y)\); 4. \(G(x \lor y) \leq G(x) \to G(y)\) and \(H(x \lor y) \leq H(x) \to H(y)\); 5. \(x \leq G(P(x))\) and \(x \leq H(F(x))\), where \(P(x) = H(x^\ast)^\ast\) and \(F = G(x^\ast)^\ast\) and \(x^\ast = x \to 0\). The justification for such an algebraic interpretation of the tense operators is given by the following theorem. Theorem. Let \(\mathcal{L} = (L; \lor, \land, \to)\) be a complete relatively pseudocomplemented lattice and \((T, \leq)\) be a frame. For \(p \in \mathcal{L}^T\) we define coordinatewise \(G(p)(x) = \bigwedge\{ p(y) ; x \leq y \} \text{ and } H(p)(x) = \bigwedge\{ p(y) ; y \leq x \}\). Then \(G,H\) are tense operators on \(\mathcal{L}^T\) satisfying the above conditions and such that \(G(0)=0=H(0)\).