2007/02/22 by Michael O'Connor, O'Connor, Michael
Computer Science · #03F55 #Advanced Algebra and Logic #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.math/0702651
openalex publication_date 2007/02/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We find a translation with particularly nice properties from intuitionistic propositional logic in countably many variables to intuitionistic propositional logic in two variables. In addition, the existence of a possibly-not-as-nice translation from any countable logic into intuitionistic propositional logic in two variables is shown. The nonexistence of a translation from classical logic into intuitionistic propositional logic which preserves ``and'' and ``or'' but not necessarily ``true'' is proven. These results about translations follow from additional results about embeddings into free Heyting algebras.