Affine logic for constructive mathematics

TL;DR

This paper demonstrates how affine logic, through an antithesis translation into intuitionistic logic, systematically derives many concepts of constructive mathematics, automating the process of constructivization.

Contribution

It introduces a systematic method using an antithesis translation of affine logic to automatically generate constructive mathematical concepts from classical ones.

Findings

Derives apartness relations and complemented subsets from affine logic

Automates the constructivization of classical concepts using the antithesis construction

Explains the bifurcation of classical concepts via affine connectives

Abstract

We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically "constructivize" classical definitions, handling the resulting bookkeeping automatically.