{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T01:33:01Z","timestamp":1777253581251,"version":"3.51.4"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T00:00:00Z","timestamp":1776124800000},"content-version":"unspecified","delay-in-days":103,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    It is well known that over Heyting arithmetic with finite types, the effective principle of the formal Church thesis, stating that all number-theoretic functional relations are computable, is inconsistent with Brouwer\u2019s intuitionistic principles on the continuum, in particular, the fan theorem. Here, we build two arithmetic quasi-toposes, validating on the one hand Brouwer\u2019s continuity principles, including the Fan theorem, and on the other hand, a restricted form of Church\u2019s Thesis, called the\n                    <jats:italic>Type-theoretic Church Thesis<\/jats:italic>\n                    and written\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline1.png\"\/>\n                        <jats:tex-math>$\\textsf{TCT}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , expressing that all morphisms of the considered quasi-topos are computable. One quasi-topos is constructed by formalizing the category of assemblies\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline2.png\"\/>\n                        <jats:tex-math>$\\mathbf{Asm}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    within Hyland\u2019s effective topos using intuitionistic Zermelo-Fraenkel set theory\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline3.png\"\/>\n                        <jats:tex-math>$\\mathbf{IZF}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    extended with Brouwer\u2019s continuity principles as our meta-theory. The other quasi-topos is obtained as an elementary quotient completion in the same intuitionistic meta-theory. While in previous work by the first author with F. Pasquali and G. Rosolini, it has been shown that these two quasi-toposes are equivalent when working within the classical\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline4.png\"\/>\n                        <jats:tex-math>$\\mathbf{ZFC}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    set theory; here, we show that this is no longer the case when working within\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline5.png\"\/>\n                        <jats:tex-math>$\\mathbf{IZF}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . We also observe that the aforementioned inconsistency is resolved in such quasi-toposes by the non-validity of the axiom of unique choice on the natural numbers and that no non-trivial topos can validate the effective principle\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129526100528_inline6.png\"\/>\n                        <jats:tex-math>$\\textsf{TCT}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    together with Brouwer\u2019s continuity principles altogether.\n                  <\/jats:p>","DOI":"10.1017\/s0960129526100528","type":"journal-article","created":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T08:49:33Z","timestamp":1776156573000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Effectiveness and continuity in intuitionistic quasi-toposes of assemblies"],"prefix":"10.1017","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9198-066X","authenticated-orcid":false,"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/00240q980","id-type":"ROR","asserted-by":"publisher"}],"name":"Universit\u00e0 degli Studi di Padova"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Sabelli","sequence":"additional","affiliation":[{"name":"Czech Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4509-594X","authenticated-orcid":false,"given":"Davide","family":"Trotta","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/00240q980","id-type":"ROR","asserted-by":"publisher"}],"name":"Universit\u00e0 degli Studi di Padova"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2026,4,14]]},"reference":[{"key":"S0960129526100528_ref31","unstructured":"Maietti, M. E. , Pasquali, F. and Rosolini, G. (2023). Quasitoposes as elementary quotient completions. Preprint, available at https:\/\/arxiv.org\/abs\/2111.15299"},{"key":"S0960129526100528_ref41","unstructured":"Menni, M. (2000). Exact Completions and Toposes. PhD thesis, School of Informatics, University of Edinburgh."},{"key":"S0960129526100528_ref27","unstructured":"Maietti, M. E. (2012). Consistency of the Minimalist Foundation with Church thesis and Bar Induction. Preprint, available at http:\/\/www.math.unipd.it\/\u223cmaietti\/pubb.html."},{"key":"S0960129526100528_ref3","volume-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"S0960129526100528_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005810"},{"key":"S0960129526100528_ref13","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198505242.001.0001"},{"key":"S0960129526100528_ref35","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"S0960129526100528_ref49","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Troelstra","year":"1988"},{"key":"S0960129526100528_ref21","first-page":"205","article-title":"Tripos theory","volume":"88","author":"Hyland","year":"1980","journal-title":"Bulletin of the Australian Mathematical Society"},{"key":"S0960129526100528_ref38","doi-asserted-by":"publisher","DOI":"10.70930\/tac\/4suml7y0"},{"key":"S0960129526100528_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663"},{"key":"S0960129526100528_ref44","doi-asserted-by":"publisher","DOI":"10.2307\/2274658"},{"key":"S0960129526100528_ref50","volume-title":"Realizability: an Introduction to Its Categorical Side","author":"van Oosten","year":"2008"},{"key":"S0960129526100528_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-013-9360-5"},{"key":"S0960129526100528_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(96)00115-6"},{"key":"S0960129526100528_ref1","volume-title":"Toposes, Triples and Theories","author":"Barr","year":"1984"},{"key":"S0960129526100528_ref29","doi-asserted-by":"publisher","DOI":"10.1515\/tmj-2017-0106"},{"key":"S0960129526100528_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7643-8653-5_18"},{"key":"S0960129526100528_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0960129526100528_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s11787-013-0080-2"},{"key":"S0960129526100528_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2024.103524"},{"key":"S0960129526100528_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004962"},{"key":"S0960129526100528_ref30","article-title":"Elementary quotient completions, Church\u2019s thesis, and partitioned assemblies","volume":"15","author":"Maietti","year":"2019","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129526100528_ref37","doi-asserted-by":"publisher","DOI":"10.12775\/LLP.2013.010"},{"key":"S0960129526100528_ref23","volume-title":"Introduction to Higher Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"S0960129526100528_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066773"},{"key":"S0960129526100528_ref28","first-page":"21","article-title":"A realizability semantics for inductive formal topologies, Church\u2019s thesis and Axiom of choice","volume":"17","author":"Maietti","year":"2021","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129526100528_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)00103-P"},{"key":"S0960129526100528_ref14","doi-asserted-by":"crossref","unstructured":"Fourman, M. and Grayson, R. J. (1982). Formal spaces. In: The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), vol. 110 of Stud. Logic Foundations Math., North-Holland, 107\u2013122.","DOI":"10.1016\/S0049-237X(09)70126-0"},{"key":"S0960129526100528_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00192-9"},{"key":"S0960129526100528_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2014.10.005"},{"key":"S0960129526100528_ref20","doi-asserted-by":"crossref","unstructured":"Hyland, J. M. E. (1982). The Effective Topos. In: The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), vol. 110 of Stud. Logic Foundations Math., Amsterdam-New York: North-Holland, 165\u2013216.","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"S0960129526100528_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19020-1_2"},{"key":"S0960129526100528_ref9","doi-asserted-by":"publisher","DOI":"10.4115\/jla.2013.5.2"},{"key":"S0960129526100528_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129526100528_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.01.006"},{"key":"S0960129526100528_ref39","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1102022209"},{"key":"S0960129526100528_ref45","first-page":"227","article-title":"Un modello per la teoria intuizionista degli insiemi","volume":"1","author":"Rosolini","year":"1982","journal-title":"Atti Degli Incontri Di Logica Matematica"},{"key":"S0960129526100528_ref17","first-page":"868","article-title":"Set-theoretic foundations for constructive analysis","volume":"19","author":"Friedman","year":"1977","journal-title":"Annals of Mathematics"},{"key":"S0960129526100528_ref40","volume-title":"Realizability and Recursive Mathematics","author":"McCarty","year":"1984"},{"key":"S0960129526100528_ref25","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0013"},{"key":"S0960129526100528_ref43","first-page":"2008","article-title":"Constructive Set Theory and Brouwerian Principles","volume":"11","author":"Rathjen","year":"2005","journal-title":"The Journal of Universal Computer Science"},{"key":"S0960129526100528_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/BF01469380"},{"key":"S0960129526100528_ref22","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"Johnstone","year":"2002"},{"key":"S0960129526100528_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705655"},{"key":"S0960129526100528_ref19","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129526100528_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"S0960129526100528_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950200364X"},{"key":"S0960129526100528_ref10","first-page":"239","volume-title":"Pillars of Enduring Strength, Learning from Hermann Weyl","author":"Contente","year":"2025"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129526100528","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T00:46:29Z","timestamp":1777250789000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129526100528\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":49,"alternative-id":["S0960129526100528"],"URL":"https:\/\/doi.org\/10.1017\/s0960129526100528","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"\u00a9 The Author(s), 2026. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e14"}}