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 (¬ , ∼) and dual Galois pair (¬ ˙ , ∼ ˙) 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 S 4 N t which is obtained from the minimal tense extension of the modal logic S 4 by adding tense operators. We give a new extended Gödel translation τ and prove that IGN is embedded into S 4 N t by τ . Moreover, every Kripke-complete Galois negation logic L is embedded into its tense companion τ (L) . [ABSTRACT FROM AUTHOR]