Kuroda's Translation for Higher-Order Logic

TL;DR

This work extends Kuroda's double-negation translation to higher-order logic and analyzes two core properties: soundness and characterization. It shows that a direct, extensionality-free route yields soundness from classical to intuitionistic HOL, while functional extensionality can destroy this property unless a weak form Δ^{f} or double-negation shift is assumed. The paper then identifies a precise necessary-and-sufficient condition, Kuroda-equivalence, for the characterization property to hold in HOL, and proves that combining functional and propositional extensionality ensures A and its Ku-translation A^{Ku} are classically equivalent. The results elucidate when Kuroda's translation preserves both truth and meaning in HOL and connect these conditions to broader themes like DNS and Takeuti-Gandy translations, with practical implications for formalizing classical reasoning inside intuitionistic frameworks.

Abstract

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.

Figures (2)

• Figure 1: Natural deduction rules for higher-order logic.
• Figure 2: Natural deduction rules for equality.

Theorems & Definitions (22)

• Proposition 1
• proof
• Definition 1: Kuroda's translation for higher-order logic
• Proposition 2
• proof
• Corollary 1
• Proposition 3
• proof
• Corollary 2
• Theorem 1