Intuitionistic Propositional Logic with Galois Negations

Intuitionistic propositional logic with Galois negations (IGN) is introduced. Heyting algebras with Galois negations are obtained from Heyting algebras by adding the Galois pair ((sic), similar to) and dual Galois pair ((sic), (similar to) over dot) of negations. Discrete duality between GN-frames and algebras as well as the relational semantics for IGN are developed. A Hilbert-style axiomatic system HN is given for IGN, and Galois negation logics are defined as extensions of IGN. We give the bi-tense logic S4N(t) which is obtained from the minimal tense extension of the modal logic S4 by adding tense operators. We give a new extended Godel translation tau and prove that IGN is embedded into S4N(t) by tau. Moreover, every Kripke-complete Galois negation logic L is embedded into its tense companion tau(L).