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.
arXiv comments
51 pages. v2: More general and precise treatment of semantics, using categories instead of posets, and hyperdoctrines and comprehension instead of triposes. Changed name to "antithesis translation" and more properly emphasized "affine" over "linear". v3-4: minor fixes; final version to appear in BSL
Linked by 2 identifiable commenters in 2 comments across 2 threads, from Jul 2018 to Nov 2018. Found in 2 HN submissions from Jul 2018 to Mar 2024. Open submission discussions.
Constructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (https://arxiv.org/abs/1805.07518). This correspondence is unreal as constructive mathematics / linear logic unlocks the door to several key advantages such as being closer to…
One of the most amazing things about linear logic is that "classical" linear logic has a direct constructive reading. This has some interesting applications in constructive mathematics (https://arxiv.org/abs/1805.07518) and programming…
Constructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (https://arxiv.org/abs/1805.07518). This correspondence is unreal as constructive mathematics / linear logic unlocks the door to several key advantages such as being closer to…
adamnemecekView on HNParent context