A Correct Polynomial Translation of S4 into intuitionistic Logic.

We show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernandez is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.