Maria Emilia Maietti ; Samuele Maschio ; Michael Rathjen - Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice

lmcs:7321 - Logical Methods in Computer Science, November 14, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:5)2022
Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of ChoiceArticle

Authors: Maria Emilia Maietti ; Samuele Maschio ; Michael Rathjen

    In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive definitions sufficient to generate Sambin's Positive topologies, namely Martin-Löf-Sambin formal topologies equipped with a Positivity relation (used to describe pointfree formal closed subsets). In particular the intensional level of MFcind, called mTTcind, is defined by extending with coinductive definitions another theory mTTind extending the intensional level mTT of MF with the sole addition of inductive definitions. In previous work we have shown that mTTind is consistent with Formal Church's Thesis CT and the Axiom of Choice AC via an interpretation in Aczel's CZF+REA. Our aim is to show the expectation that the addition of coinductive definitions to mTTind does not increase its consistency strength by reducing the consistency of mTTcind+CT+AC to the consistency of CZF+REA through various interpretations. We actually reach our goal in two ways. One way consists in first interpreting mTTcind+CT+AC in the theory extending CZF with the Union Regular Extension Axiom, REA_U, a strengthening of REA, and the Axiom of Relativized Dependent Choice, RDC. The theory CZF+REA_U+RDC is then interpreted in MLS*, a version of Martin-Löf's type theory with Palmgren's superuniverse S. A last step consists in interpreting MLS* back into CZF+REA. The alternative way consists in first interpreting mTTcind+AC+CT directly in a version of Martin-Löf's type theory with Palmgren's superuniverse extended with CT, which is then interpreted back to CZF+REA. A key benefit of the first way is that the theory CZF+REA_U+RDC also supports the intended set-theoretic interpretation of the extensional level of MFcind. Finally, all the theories considered, except mTTcind+AC+CT, are shown to be of the same proof-theoretic strength.


    Volume: Volume 18, Issue 4
    Published on: November 14, 2022
    Accepted on: September 28, 2022
    Submitted on: April 1, 2021
    Keywords: Mathematics - Logic,03B38, 03F03, 03F50,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1298 times.
    This article's PDF has been downloaded 397 times.