Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti

Thomas Traversié

TL;DR

This work addresses translating classical proofs into intuitionistic ones within the lambdaPi-calculus modulo theory, a framework that combines dependent types and user-defined rewrite rules in Dedukti. The authors extend Kuroda's double-negation translation to theories encoded in higher-order logic, formalize the embedding of classical into intuitionistic logic, and implement the translation in Construkti to produce translated Dedukti proofs. They demonstrate the approach by translating and benchmarking a substantial library of proofs (including propositional, first-order, and higher-order results) and report successful typechecking of all translated proofs. The results enable interoperability between classical proof systems and intuitionistic proof assistants, facilitating cross-system proof exchange and verification.

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.

Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti

TL;DR

This work addresses translating classical proofs into intuitionistic ones within the lambdaPi-calculus modulo theory, a framework that combines dependent types and user-defined rewrite rules in Dedukti. The authors extend Kuroda's double-negation translation to theories encoded in higher-order logic, formalize the embedding of classical into intuitionistic logic, and implement the translation in Construkti to produce translated Dedukti proofs. They demonstrate the approach by translating and benchmarking a substantial library of proofs (including propositional, first-order, and higher-order results) and report successful typechecking of all translated proofs. The results enable interoperability between classical proof systems and intuitionistic proof assistants, facilitating cross-system proof exchange and verification.

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.
Paper Structure (18 sections, 12 theorems, 12 equations, 1 figure, 1 table)

This paper contains 18 sections, 12 theorems, 12 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Contribution.
  3. Outline of the paper.
  4. Higher-Order Logic in the lambdaPi-Calculus Modulo Theory
  5. The lambdaPi-Calculus Modulo Theory
  6. An Encoding of Higher-Order Logic
  7. Theories Encoded in Higher-Order Logic
  8. Kuroda's Translation in the lambdaPi-Calculus Modulo Theory
  9. Translation of Terms and Theories
  10. Embedding Classical Logic into Intuitionistic Logic
  11. Back to the Original Theory
  12. Construkti, an Implementation for Dedukti Proofs
  13. Dedukti.
  14. Construkti.
  15. Benchmark.
  16. ...and 3 more sections

Key Result

Lemma 1

If $\Gamma \vdash t : A$, then either $A = \hbox{\tt KIND}$ or $\Gamma \vdash A : s$ for $s = \hbox{\tt TYPE}$ or $s = \hbox{\tt KIND}$. If $\Gamma \vdash \Pi x : A. ~B : s$, then $\Gamma \vdash A : \hbox{\tt TYPE}$.

Figures (1)

  • Figure 1: Typing rules of the $\lambda \Pi$-calculus modulo theory.

Theorems & Definitions (30)

  • Lemma 1
  • Definition 1: $\kappa$-property
  • Definition 2: Theory encoded in higher-order logic
  • Example 1: Equational theory
  • Definition 3: Translation of terms
  • Proposition 1
  • proof
  • Definition 4
  • Definition 5: Translation of theories
  • Lemma 2: Translation of substitutions
  • ...and 20 more