{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:11Z","timestamp":1753894391667,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,11,14]],"date-time":"2022-11-14T00:00:00Z","timestamp":1668384000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In this work we consider an extension MFcind of the Minimalist Foundation MF\nfor predicative constructive mathematics with the addition of inductive and\ncoinductive definitions sufficient to generate Sambin's Positive topologies,\nnamely Martin-L\\\"of-Sambin formal topologies equipped with a Positivity\nrelation (used to describe pointfree formal closed subsets). In particular the\nintensional level of MFcind, called mTTcind, is defined by extending with\ncoinductive definitions another theory mTTind extending the intensional level\nmTT of MF with the sole addition of inductive definitions. In previous work we\nhave shown that mTTind is consistent with Formal Church's Thesis CT and the\nAxiom of Choice AC via an interpretation in Aczel's CZF+REA. Our aim is to show\nthe expectation that the addition of coinductive definitions to mTTind does not\nincrease its consistency strength by reducing the consistency of mTTcind+CT+AC\nto the consistency of CZF+REA through various interpretations. We actually\nreach our goal in two ways. One way consists in first interpreting\nmTTcind+CT+AC in the theory extending CZF with the Union Regular Extension\nAxiom, REA_U, a strengthening of REA, and the Axiom of Relativized Dependent\nChoice, RDC. The theory CZF+REA_U+RDC is then interpreted in MLS*, a version of\nMartin-L\\\"of's type theory with Palmgren's superuniverse S. A last step\nconsists in interpreting MLS* back into CZF+REA. The alternative way consists\nin first interpreting mTTcind+AC+CT directly in a version of Martin-L\\\"of's\ntype theory with Palmgren's superuniverse extended with CT, which is then\ninterpreted back to CZF+REA. A key benefit of the first way is that the theory\nCZF+REA_U+RDC also supports the intended set-theoretic interpretation of the\nextensional level of MFcind. Finally, all the theories considered, except\nmTTcind+AC+CT, are shown to be of the same proof-theoretic strength.<\/jats:p>","DOI":"10.46298\/lmcs-18(4:5)2022","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T15:20:50Z","timestamp":1669130450000},"source":"Crossref","is-referenced-by-count":0,"title":["Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice"],"prefix":"10.46298","volume":"Volume 18, Issue 4","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuele","family":"Maschio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Rathjen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2022,11,14]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/10299\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/10299\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:19:43Z","timestamp":1687292383000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7321"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,14]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(4:5)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2103.16592v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2103.16592v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2103.16592v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2103.16592","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2103.16592","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,11,14]]},"article-number":"7321"}}