{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T14:10:09Z","timestamp":1756735809096,"version":"3.44.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"FWF","award":["TAI-797"],"award-info":[{"award-number":["TAI-797"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2025,10,31]]},"abstract":"\n Das, van der Giessen, and Marin recently introduced\n \n \\(\\mathsf{IGL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , an intuitionistic version of G\u00f6del-L\u00f6b logic. Their proof systems involves ill-founded proofs with a progressiveness condition. Their completeness proof uses the principle of\n \n \\(\\Sigma^{1}_{1}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -determinacy; which is not provable in\n \n \\(\\mathsf{ZFC}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . We define a cyclic proof system for\n \n \\(\\mathsf{IGL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and give a proof of its completeness theorem avoiding\n \n \\(\\Sigma^{1}_{1}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -determinacy.\n <\/jats:p>","DOI":"10.1145\/3748649","type":"journal-article","created":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T13:25:48Z","timestamp":1752672348000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Intuitionistic G\u00f6del-L\u00f6b without Sharps"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2768-6714","authenticated-orcid":false,"given":"Juan P.","family":"Aguilera","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, TU Wien, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7703-7990","authenticated-orcid":false,"given":"Leonardo","family":"Pacheco","sequence":"additional","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, TU Wien, Wien, Austria and Institute of Science Tokyo, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63501-4_13"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.4230\/lipics.fsttcs.2023.40"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2024.22"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Gis\u00e8le Fischer Servi. 1977. On modal logic with an intuitionistic base. Studia Logica 36 3 (1977) 141\u2013149. DOI: 10.1007\/BF02121259","DOI":"10.1007\/BF02121259"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400881970-014"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Leo Harrington. 1978. Analytic determinacy and \\(0^{:}textnum:\\) . Journal of Symbolic Logic 43 4 (1978) 685\u2013693. DOI: 10.2307\/2273508","DOI":"10.2307\/2273508"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Donald A. Martin. 1970. Measurable cardinals and analytic games. Fundamenta Mathematicae 66 (1970) 287\u2013291.","DOI":"10.4064\/fm-66-3-287-291"},{"key":"e_1_3_2_9_2","unstructured":"Mojtaba Mojtahedi. 2022. On provability logic of HA. arXiv: 2206.00445. Retrieved from https:\/\/arxiv.org\/abs\/2206.00445"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Daniyar Salkarbekovich Shamkanov. 2014. Circular proofs for the G\u00f6del-L\u00f6b provability logic. Mathematical Notes 96 (2014) 575\u2013585.","DOI":"10.1134\/S0001434614090326"},{"key":"e_1_3_2_11_2","unstructured":"Alex K. Simpson. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. Dissertation. University of Edinburgh. Retrieved from https:\/\/era.ed.ac.uk\/handle\/1842\/407"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Robert M. Solovay. 1976. Provability interpretations of modal logic. 25 3 (1976) 287\u2013304. DOI: 10.1007\/BF02757006","DOI":"10.1007\/BF02757006"},{"key":"e_1_3_2_13_2","unstructured":"John R. Steel. 1977. Determinateness and Subsystems of Analysis. Ph.D. Dissertation."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Iris van der Giessen. 2022. Uniform Interpolation and Admissible Rules: Proof-Theoretic Investigations into (Intuitionistic) Modal Logics. Ph.D. Dissertation. Utrecht University. DOI: 10.33540\/1486","DOI":"10.33540\/1486"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3748649","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T13:43:19Z","timestamp":1756734199000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3748649"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9]]},"references-count":13,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,10,31]]}},"alternative-id":["10.1145\/3748649"],"URL":"https:\/\/doi.org\/10.1145\/3748649","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2025,9]]},"assertion":[{"value":"2024-09-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-02","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}