In 1951, Kuroda defined an embedding of classical first-order 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, but did not prove the classical equivalence, and showed that the embedding fails in the presence of functional extensionality. We prove that functional extensionality and propositional extensionality are sufficient to derive the classical equivalence between a higher-order formula and its translation. We emphasize a condition under which Kuroda's translation works with functional extensionality.

翻译：1951年，Kuroda定义了经典一阶逻辑到直觉主义逻辑的嵌入，使得公式及其翻译在经典逻辑中等价。最近，Brown和Rizkallah将这一翻译扩展到了高阶逻辑，但未证明经典等价性，并表明该嵌入在函数外延性存在时失效。我们证明函数外延性和命题外延性足以推导出高阶公式与其翻译之间的经典等价性。我们着重阐述了Kuroda翻译在函数外延性下成立的条件。