Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic

Michael O'Connor

We find a translation with particularly nice properties from intuitionistic propositional logic in countably many variables to intuitionistic propositional logic in two variables.…