Negative Translations for Affine and Lukasiewicz Logic

TL;DR

This paper examines four classical-to-intuitionistic negative translations within affine and Lukasiewicz logic, revealing which schemes satisfy Troelstra's criteria and their equivalences in Lukasiewicz logic.

Contribution

It provides a detailed analysis of negative translation schemes in substructural logics, showing their validity and equivalence in different logical frameworks.

Findings

Kolmogorov and G"odel translations satisfy Troelstra's criteria in affine logic.

Glivenko and Gentzen translations fail in affine logic for different reasons.

All studied translations are equivalent in Lukasiewicz logic.

Abstract

We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schemes due to Kolmogorov and G\"odel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and vice versa. By contrast, in the setting of Lukasiewicz logic, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, G\"odel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Lukasiewicz logic but are all equivalent.