Kuroda's Translation for Higher-Order Logic
This work clarifies theoretical limitations in logic translations for researchers in mathematical logic and proof theory, though it appears incremental as it builds on prior extensions.
The paper addresses the failure of Kuroda's translation in higher-order logic with functional extensionality, showing that classical equivalence between a formula and its translation does not generally hold, but can be achieved by assuming both functional and propositional extensionality.
Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic. However, they showed that the translation fails in the presence of functional extensionality, and they did not prove the classical equivalence between a formula and its translation. In this paper, 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 classical equivalence between a formula and its translation does not necessarily hold in higher-order logic. However, it is sufficient to assume both functional extensionality and propositional extensionality.