{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:23:14Z","timestamp":1740108194325,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:00:00Z","timestamp":1718668800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:00:00Z","timestamp":1718668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2025,2]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>It has long been known that (classical) Peano arithmetic is, in some strong sense, \u201cequivalent\u201d to the variant of (classical) Zermelo\u2013Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. We present an intuitionistic theory of the hereditarily finite sets, and show that it is definitionally equivalent to Heyting Arithmetic , in a sense to be made precise. Our main target theory, the intuitionistic small set theory  is remarkably simple, and intuitive. It has just one non-logical primitive, for membership, and three straightforward axioms plus one axiom scheme. We locate our theory within intuitionistic mathematics generally.<\/jats:p>","DOI":"10.1007\/s00153-024-00935-4","type":"journal-article","created":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T10:02:06Z","timestamp":1718704926000},"page":"79-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Intuitionistic sets and numbers: small set theory and Heyting arithmetic"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4895-0772","authenticated-orcid":false,"given":"Stewart","family":"Shapiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"McCarty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Rathjen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,18]]},"reference":[{"key":"935_CR1","doi-asserted-by":"crossref","unstructured":"Ackermann, W.: Die Widerspruchsfreiheit der allgemeinen Mengenlehre. [The consistency of general set theory]. Math. Ann. [Ann. Math.] 114, 305\u2013315 (1937)","DOI":"10.1007\/BF01594179"},{"key":"935_CR2","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0049-237X(08)71989-X","volume-title":"Logic Colloquium \u201977","author":"P Aczel","year":"1978","unstructured":"Aczel, P.: The type theoretic interpretation of constructive set theory. In: MacIntyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium \u201977, pp. 55\u201366. North Holland, Amsterdam (1978)"},{"key":"935_CR3","doi-asserted-by":"crossref","unstructured":"Aczel, P.: The type theoretic interpretation of constructive set theory: choice principles. In: Troelstra, A.S., van Dalen, D. (eds.) The L.E.J. Brouwer Centenary Symposium, pp. 1\u201340. North Holland, Amsterdam (1982)","DOI":"10.1016\/S0049-237X(09)70120-X"},{"key":"935_CR4","first-page":"17","volume-title":"Logic, Methodology and Philosophy of Science VII","author":"P Aczel","year":"1986","unstructured":"Aczel, P.: The type theoretic interpretation of constructive set theory: inductive definitions. In: Marcus, R.B., et al. (eds.) Logic, Methodology and Philosophy of Science VII, pp. 17\u201349. North Holland, Amsterdam (1986)"},{"key":"935_CR5","unstructured":"Aczel, P.: Non-well-founded sets. Center for the Study of Language and Information, Stanford (1988)"},{"key":"935_CR6","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical Report 40, Institut Mittag\u2013Leffler. The Royal Swedish Academy of Sciences. http:\/\/www.ml.kva.se\/preprints\/archive2000-2001.php (2001)"},{"key":"935_CR7","unstructured":"Aczel, P., Rathjen, M.: Constructive set theory. Book draft, 2010, available at (2010) http:\/\/www1.maths.leeds.ac.uk\/~rathjen\/book.pdf"},{"issue":"6","key":"935_CR8","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1002\/malq.200410051","volume":"51","author":"H Andr\u00e9ka","year":"2005","unstructured":"Andr\u00e9ka, H., Madar\u00e1sz, J., N\u00e9meti, I.: Mutual definability does not imply definitional equivalence, a simple example. Math. Logic Q. 51(6), 591\u2013597 (2005)","journal-title":"Math. Logic Q."},{"key":"935_CR9","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Foundations of Constructive Mathematics. Metamathematical Studies, p. XXIII+466. Springer-Verlag, Berlin (1985)","DOI":"10.1007\/978-3-642-68952-9"},{"issue":"4","key":"935_CR10","first-page":"477","volume":"11","author":"GE Collins","year":"1970","unstructured":"Collins, G.E., Halpern, J.D.: On the interpretability of arithmetic in set theory. Notre Dame J. Form. Logic 11(4), 477\u2013483 (1970)","journal-title":"Notre Dame J. Form. Logic"},{"key":"935_CR11","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1017\/bsl.2017.30","volume":"23","author":"Z Damnjanovic","year":"2017","unstructured":"Damnjanovic, Z.: Mutual interpretability of Robinson arithmetic and adjunctive set theory with extensionality. Bull. Symb. Logic 23, 381\u2013404 (2017)","journal-title":"Bull. Symb. Logic"},{"key":"935_CR12","unstructured":"Friedman, H., Visser, A.: When Bi-interpretability Implies Synonymy. https:\/\/dspace.library.uu.nl\/handle\/1874\/308486 (2014)"},{"key":"935_CR13","unstructured":"Jeon, H.: Constructive Ackermann Interpretation. arxiv:2010.04270 (2020)"},{"key":"935_CR14","first-page":"497","volume":"4","author":"R Kaye","year":"2007","unstructured":"Kaye, R., Wong, T.L.: On interpretations of arithmetic and set theory. Notre Dame J. Form. Logic 4, 497\u2013510 (2007)","journal-title":"Notre Dame J. Form. Logic"},{"issue":"3","key":"935_CR15","first-page":"227","volume":"50","author":"L Kirby","year":"2009","unstructured":"Kirby, L.: Finitary set theory. Notre Dame J. Form. Logic 50(3), 227\u2013244 (2009)","journal-title":"Notre Dame J. Form. Logic"},{"issue":"4","key":"935_CR16","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S Kleene","year":"1945","unstructured":"Kleene, S.: On the interpretation of intuitionistic number theory. J. Symb. Logic 10(4), 109\u2013124 (1945)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"935_CR17","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.indag.2017.10.003","volume":"29","author":"T Litak","year":"2018","unstructured":"Litak, T., Visser, A.: Lewis meets Brouwer, constructive strict implication. Indag. Math. 29(1), 36\u201390 (2018)","journal-title":"Indag. Math."},{"key":"935_CR18","unstructured":"McCarty, C.: Realizability and Recursive Mathematics, p. 281. Department of Computer Science. Carnegie-Mellon University, Pittsburgh, PA. Report Number CMU-CS-84-131 (1984)"},{"issue":"4","key":"935_CR19","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.2307\/2274603","volume":"53","author":"C McCarty","year":"1988","unstructured":"McCarty, C.: Constructive validity is nonarithmetic. J. Symb. Logic 53(4), 1036\u20131041 (1988)","journal-title":"J. Symb. Logic"},{"key":"935_CR20","first-page":"186","volume":"35","author":"F Montagna","year":"1994","unstructured":"Montagna, F., Mancini, A.: A minimal predicative set theory. Notre Dame J. Form. Logic 35, 186\u2013203 (1994)","journal-title":"Notre Dame J. Form. Logic"},{"key":"935_CR21","unstructured":"Moschovakis, Y.N.: Recursion in the Universe of Sets, Mimeographed Note (1976)"},{"key":"935_CR22","first-page":"64","volume":"3","author":"J Mycielski","year":"1964","unstructured":"Mycielski, J.: The definition of arithmetic operations in the Ackermann model. Algebra Log. Semin. 3, 64\u201365 (1964)","journal-title":"Algebra Log. Semin."},{"key":"935_CR23","doi-asserted-by":"crossref","unstructured":"Mycielski, J., Pudl\u00e1k, P., Stern, A.S.: A Lattice of Chapters of Mathematics (Interpretations Between Theorems), Volume 84 of Memoirs of the American Mathematical Society. AMS, Providence (1990)","DOI":"10.1090\/memo\/0426"},{"key":"935_CR24","doi-asserted-by":"publisher","first-page":"347","DOI":"10.2307\/2272159","volume":"40","author":"J Myhill","year":"1975","unstructured":"Myhill, J.: Constructive set theory. J. Symb. Logic 40, 347\u2013382 (1975)","journal-title":"Constructive set theory. J. Symb. Logic"},{"key":"935_CR25","doi-asserted-by":"publisher","DOI":"10.1515\/9781400858927","volume-title":"Predicative Arithmetic","author":"E Nelson","year":"1986","unstructured":"Nelson, E.: Predicative Arithmetic. Princeton University Press, Princeton (1986)"},{"key":"935_CR26","doi-asserted-by":"crossref","unstructured":"Normann, D.: Set recursion. In: Generalized Recursion Theory II, pp. 303\u2013320. North-Holland, Amsterdam (1978)","DOI":"10.1016\/S0049-237X(08)70938-8"},{"key":"935_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","volume":"55","author":"L Paulson","year":"2015","unstructured":"Paulson, L.: A mechanized proof of G\u00f6del\u2019s incompleteness theorems using nominal Isabelle. J. Autom. Reason. 55, 1\u201337 (2015)","journal-title":"J. Autom. Reason."},{"key":"935_CR28","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF01203033","volume":"33","author":"F Previale","year":"1994","unstructured":"Previale, F.: Induction and foundation in the theory of hereditarily finite sets. Arch. Math. Logic 33, 213\u2013241 (1994)","journal-title":"Arch. Math. Logic"},{"key":"935_CR29","doi-asserted-by":"crossref","unstructured":"Rathjen, M.: Realizability for constructive Zermelo\u2013Fraenkel set theory. In: V\u00e4\u00e4n\u00e4nen, J., Stoltenberg-Hansen, V. (eds.) Logic Colloquium 2003. Lecture Notes in Logic 24, pp. 282\u2013314. A.K. Peters (2006)","DOI":"10.1201\/9781439865835-14"},{"key":"935_CR30","doi-asserted-by":"publisher","first-page":"1400","DOI":"10.1016\/j.apal.2012.01.012","volume":"163","author":"M Rathjen","year":"2012","unstructured":"Rathjen, M.: From the weak to the strong existence property. Ann. Pure Appl. Logic 163, 1400\u20131418 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"935_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-12013-2","volume-title":"Higher Recursion Theory","author":"GE Sacks","year":"1990","unstructured":"Sacks, G.E.: Higher Recursion Theory. Springer, Berlin (1990)"},{"key":"935_CR32","unstructured":"Shoenfield, J.: Mathematical Logic, p. vii+344. Addison-Wesley, Boston (1967)"},{"key":"935_CR33","unstructured":"Szmielew, W., Tarski, A.: Mutual Interpretability of some essentially undecidable theories. In: Proceedings of the International Congress of Mathematicians (Cambridge, Massachusetts, 1950), vol. 1, p. 734. American Mathematical Society, Providence (1952)"},{"key":"935_CR34","first-page":"1","volume":"422","author":"S \u015awierczkowski","year":"2003","unstructured":"\u015awierczkowski, S.: Finite sets and G\u00f6del\u2019s incompleteness theorems. Diss. Math. 422, 1\u201358 (2003)","journal-title":"Diss. Math."},{"key":"935_CR35","unstructured":"Tarski, A., Mostowski, A., Robinson. R.M.: Undecidable Theories. North-Holland, Amsterdam (1953)"},{"key":"935_CR36","doi-asserted-by":"crossref","unstructured":"Troelstra, A.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Lecture Notes in Mathematics, vol. 344, p. XVII+485. Springer-Verlag, Berlin (1973)","DOI":"10.1007\/BFb0066739"},{"key":"935_CR37","unstructured":"Troelstra, A., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol. 1, p. xx+342. North-Holland Publishing Company, Amsterdam (1988)"},{"key":"935_CR38","unstructured":"van Oosten, J.: Realizability: An Introduction to its Categorical Side, p. viii+328. Elsevier Science, Amsterdam (2008)"},{"key":"935_CR39","doi-asserted-by":"crossref","unstructured":"Visser, A.: Categories of Theories and Interpretations. Logic in Tehran. Lecture Notes in Logic. Association for Symbolic Logic, vol. 26, pp. 284\u2013341. Cambridge University Press, La Jolla (2006)","DOI":"10.1201\/9781439865873-16"},{"issue":"3","key":"935_CR40","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1017\/S1755020309090261","volume":"2","author":"A Visser","year":"2009","unstructured":"Visser, A.: Cardinal arithmetic in the style of Baron von M\u00fcnchhausen. Rev. Symb. Logic 2(3), 570\u2013589 (2009)","journal-title":"Rev. Symb. Logic"},{"key":"935_CR41","doi-asserted-by":"publisher","first-page":"942","DOI":"10.2307\/2275794","volume":"61","author":"D Zambella","year":"1996","unstructured":"Zambella, D.: Notes on polynomially bounded arithmetic. J. Symb. Logic 61, 942\u2013966 (1996)","journal-title":"J. Symb. Logic"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00935-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-024-00935-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00935-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T05:40:42Z","timestamp":1739338842000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-024-00935-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,18]]},"references-count":41,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2025,2]]}},"alternative-id":["935"],"URL":"https:\/\/doi.org\/10.1007\/s00153-024-00935-4","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2024,6,18]]},"assertion":[{"value":"19 February 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}