Benno van den Berg ; Robert Passmann - Converse extensionality and apartness

lmcs:7306 - Logical Methods in Computer Science, December 20, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:13)2022
Converse extensionality and apartnessArticle

Authors: Benno van den Berg ; Robert Passmann

    In this paper we try to find a computational interpretation for a strong form of extensionality, which we call "converse extensionality". Converse extensionality principles, which arise as the Dialectica interpretation of the axiom of extensionality, were first studied by Howard. In order to give a computational interpretation to these principles, we reconsider Brouwer's apartness relation, a strong constructive form of inequality. Formally, we provide a categorical construction to endow every typed combinatory algebra with an apartness relation. We then exploit that functions reflect apartness, in addition to preserving equality, to prove that the resulting categories of assemblies model a converse extensionality principle.

    https://doi.org/10.46298/lmcs-18(4:13)2022
    Source: arXiv.org:2103.14482
    Volume: Volume 18, Issue 4
    Published on: December 20, 2022
    Accepted on: November 24, 2022
    Submitted on: March 29, 2021
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,Mathematics - Category Theory
    Licence: Attribution 4.0 International (CC BY 4.0)

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    Share and export

    Consultation statistics

    This page has been seen 1863 times.
    This article's PDF has been downloaded 272 times.