Kuroda's Translation for Higher-Order Logic

TL;DR

This paper investigates conditions under which Kuroda's translation can be extended to higher-order logic, especially considering functional and propositional extensionality, and clarifies when classical equivalence holds.

Contribution

It identifies specific conditions, including functional and propositional extensionality, that ensure Kuroda's translation's effectiveness in higher-order logic.

Findings

Kuroda's translation fails with functional extensionality alone.

Classical equivalence does not always hold in higher-order logic.

Both functional and propositional extensionality are sufficient conditions.

Abstract

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.