A Kuroda-style j-translation

TL;DR

This paper introduces a new syntactic j-translation inspired by Kuroda's negative translation, extending the existing topos-theoretic approach to intuitionistic logic without requiring topos theory knowledge.

Contribution

It presents a novel Kuroda-style j-translation that applies nuclei to implications, broadening the scope of logical translations within intuitionistic logic.

Findings

Establishes a syntactic Kuroda-style j-translation

Generalizes the negative translation approach

Does not require topos theory knowledge

Abstract

In topos theory it is well-known that any nucleus j gives rise to a translation of intuitionistic logic into itself in a way which generalises the Goedel-Gentzen negative translation. Here we show that there exists a similar j-translation which is more in the spirit of Kuroda's negative translation. The key is to apply the nucleus not only to the entire formula and universally quantified subformulas, but to conclusions of implications as well. The development is entirely syntactic and no knowledge of topos theory is required to read this small note.