Affine logic for constructive mathematics

DOI10.1017/BSL.2022.28MaRDI QIDQ6301815arXivFDO

Authors Michael Shulman

Publication date 19 May 2018

Published in arXiv

Full work available at URL https://doi.org/10.1017/BSL.2022.28

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Other constructive mathematics (03F65)

arXiv classification

math.LO

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.

This page was built for publication: Affine logic for constructive mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6301815)