Kuroda's Translation for the $\lambda\Pi$-Calculus Modulo Theory and Dedukti

TL;DR

This paper adapts Kuroda's translation for higher-order logic to the lambdaPi-calculus modulo theory, enabling embedding of classical logic into intuitionistic logic within Dedukti, a proof language based on this framework.

Contribution

It extends Kuroda's translation to the lambdaPi-calculus modulo theory and implements a tool for proof translation in Dedukti.

Findings

Successfully adapted Kuroda's translation for lambdaPi-calculus modulo theory

Developed a tool for proof translation in Dedukti

Facilitated embedding of classical logic into intuitionistic logic in the framework

Abstract

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the lambdaPi-calculus modulo theory, a logical framework that extends lambda-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in Dedukti, a proof language based on the lambdaPi-calculus modulo theory.