{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T08:11:26Z","timestamp":1774080686888,"version":"3.50.1"},"reference-count":22,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:00:00Z","timestamp":1777593600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:00:00Z","timestamp":1777593600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T00:00:00Z","timestamp":1772064000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2026,5]]},"DOI":"10.1016\/j.tcs.2026.115832","type":"journal-article","created":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T07:42:17Z","timestamp":1772264537000},"page":"115832","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Categorical structure in coherent theory of arithmetic"],"prefix":"10.1016","volume":"1071","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8983-0099","authenticated-orcid":false,"given":"Lingyuan","family":"Ye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2026.115832_bib0001","first-page":"219","article-title":"Aspects of categorical recursion theory","author":"Hofstra","year":"2021","journal-title":"Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics"},{"key":"10.1016\/j.tcs.2026.115832_bib0002","series-title":"Introduction to Higher-Order Categorical Logic","volume":"7","author":"Lambek","year":"1988"},{"issue":"3","key":"10.1016\/j.tcs.2026.115832_bib0003","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0022-4049(89)90042-X","article-title":"Cartesian categories with natural numbers object","volume":"58","author":"Rom\u00e1n","year":"1989","journal-title":"J. Pure Appl. Algebra"},{"key":"10.1016\/j.tcs.2026.115832_bib0004","series-title":"Sketches of an Elephant: A Topos Theory Compendium","volume":"1","author":"Johnstone","year":"2002"},{"key":"10.1016\/j.tcs.2026.115832_bib0005","doi-asserted-by":"crossref","DOI":"10.1017\/9781316717271","article-title":"Metamathematics of First-Order Arithmetic","author":"H\u00e1jek","year":"2017"},{"issue":"4","key":"10.1016\/j.tcs.2026.115832_bib0006","doi-asserted-by":"crossref","first-page":"1448","DOI":"10.2307\/2275651","article-title":"Minimal models of Heyting arithmetic","volume":"62","author":"Moerdijk","year":"1997","journal-title":"J. Symbol. Logic"},{"issue":"1","key":"10.1016\/j.tcs.2026.115832_bib0007","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0004972700044828","article-title":"Aspects of topoi","volume":"7","author":"Freyd","year":"1972","journal-title":"Bull. Australian Math. Soc."},{"issue":"4","key":"10.1016\/j.tcs.2026.115832_bib0008","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1305\/ndjfl\/1093870454","article-title":"On the Freyd cover of a topos","volume":"24","author":"Moerdijk","year":"1983","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/j.tcs.2026.115832_bib0009","series-title":"Theories, Sites, Toposes: Relating and Studying Mathematical Theories through Topos-Theoretic \u2019Bridges\u2019","author":"Caramello","year":"2018"},{"issue":"5","key":"10.1016\/j.tcs.2026.115832_bib0010","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1017\/S0960129599002741","article-title":"Topical categories of domains","volume":"9","author":"Vickers","year":"1999","journal-title":"Math. Struc. Comput. Sci."},{"key":"10.1016\/j.tcs.2026.115832_bib0011","series-title":"Mathematical Proceedings of the Cambridge Philosophical Society","first-page":"207","article-title":"Finiteness and decidability: II","volume":"84","author":"Johnstone","year":"1978"},{"issue":"3","key":"10.1016\/j.tcs.2026.115832_bib0012","doi-asserted-by":"crossref","first-page":"87","DOI":"10.2307\/2269028","article-title":"Extensions of some theorems of G\u00f6del and Church","volume":"1","author":"Rosser","year":"1936","journal-title":"J. Symb. Logic"},{"issue":"7","key":"10.1016\/j.tcs.2026.115832_bib0013","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1007\/s00153-015-0450-y","article-title":"Normalization proof for Peano arithmetic","volume":"54","author":"Siders","year":"2015","journal-title":"Arch. Math. Logic"},{"issue":"4","key":"10.1016\/j.tcs.2026.115832_bib0014","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1017\/S0960129500001183","article-title":"Connected limits, familial representability and Artin glueing","volume":"5","author":"Carboni","year":"1995","journal-title":"Math. Struc. Comput. Sci."},{"issue":"1","key":"10.1016\/j.tcs.2026.115832_bib0015","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0960129596002150","article-title":"Intuitionistic model constructions and normalization proofs","volume":"7","author":"Coquand","year":"1997","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/j.tcs.2026.115832_bib0016","series-title":"First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory","author":"Sterling","year":"2021"},{"key":"10.1016\/j.tcs.2026.115832_bib0017","article-title":"Bounded Arithmetic","author":"Buss","year":"1986"},{"issue":"3","key":"10.1016\/j.tcs.2026.115832_bib0018","article-title":"The G\u00f6del incompleteness theorem, a categorical approach","volume":"16","author":"Joyal","year":"2005","journal-title":"Cahiers de topologie et g\u00e9ometrie diff\u00e9rentielle categoriques"},{"key":"10.1016\/j.tcs.2026.115832_bib0019","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/S1571-0661(04)80569-3","article-title":"Joyal\u2019s arithmetic universes via type theory","volume":"69","author":"Maietti","year":"2003","journal-title":"Electron Notes Theor. Comput. Sci."},{"key":"10.1016\/j.tcs.2026.115832_bib0020","article-title":"Joyal\u2019s arithmetic universe as list-arithmetic pretopos","volume":"24","author":"Maietti","year":"2010","journal-title":"Theory Appl. Categor."},{"issue":"8\u20139","key":"10.1016\/j.tcs.2026.115832_bib0021","doi-asserted-by":"crossref","first-page":"2049","DOI":"10.1016\/j.jpaa.2012.02.040","article-title":"An induction principle for consequence in arithmetic universes","volume":"216","author":"Maietti","year":"2012","journal-title":"J. Pure Appl. Algebra"},{"key":"10.1016\/j.tcs.2026.115832_bib0022","unstructured":"J. van Dijk, A.G. Oldenziel, G\u00f6del incompleteness through arithmetic universes after A. Joyal, arXiv: 2004.10482(2020)."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397526000915?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397526000915?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T07:36:35Z","timestamp":1774078595000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397526000915"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5]]},"references-count":22,"alternative-id":["S0304397526000915"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2026.115832","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2026,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Categorical structure in coherent theory of arithmetic","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2026.115832","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Author(s). Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"115832"}}