INDUCTIVE AND COINDUCTIVE TOPOLOGICAL GENERATION WITH CHURCH'S THESIS AND THE AXIOM OF CHOICE.

In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive topological definitions sufficient to generate Sambin's Positive topologies, namely Martin-Löf-Sambin formal topologies (used to describe pointfree formal open subsets) 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 topological definitions another theory mTTind extending the intensional level mTT of MF with the sole addition of inductive topological definitions. In previous work we have shown that mTTind is consistent with adding simultaneously formal Church's Thesis, CT, and the Axiom of Choice, AC, via an interpretation in Aczel's CZF +REA, namely Constructive Zermelo-Fraenkel Set Theory with the Regular Extension Axiom. Our aim is to show the expectation that the addition of coinductive topological 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 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, REAS, a strengthening of REA, and the Axiom of Relativized Dependent Choice, RDC. The theory CZF+REAS+RDC is then interpreted in MLS, a version of Martin-Löof's type theory with Palmgren's superuniverse S. The 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 + REAS + RDC also supports the intended set-theoretic interpretation of the extensional level of MFcind. Finally, all the theories considered to reach our goals, except mTTcind+AC + CT, are shown to be of the same proof-theoretic strength. [ABSTRACT FROM AUTHOR]