KURODA’S TRANSLATION FOR HIGHER-ORDER LOGIC

Abstract Kuroda’s translation embeds first-order classical logic into first-order intuitionistic logic. It satisfies the soundness property—if a judgment is provable in classical logic, then its translation is provable in intuitionistic logic—as well as the characterization property—a formula and its translation are equivalent in classical logic—and the reverse translation property—if the translation of a judgment is provable in intuitionistic logic then the original judgment is provable in classical logic. Brown and Rizkallah extended Kuroda’s translation to higher-order logic. However, they showed that the soundness property fails in the presence of functional extensionality, and they neither proved the characterization property nor the reverse translation property. In this article, we emphasize different conditions under which Kuroda’s translation works in the presence of functional extensionality, including the double-negation shift. We show that the characterization property and the reverse translation property do not necessarily hold in higher-order logic. Nevertheless, we prove that it is sufficient to assume both functional extensionality and propositional extensionality.