{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T00:38:52Z","timestamp":1783643932163,"version":"3.55.0"},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":10784,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1984,9]]},"abstract":"<jats:p>We deal here with two modal logics, <jats:italic>GL<\/jats:italic> and <jats:italic>Grz<\/jats:italic>, that are known to have interesting arithmetical interpretations connected with the notion of provability. <jats:italic>GL<\/jats:italic> is the extensiom of <jats:italic>K<\/jats:italic> (or <jats:italic>K<\/jats:italic>4) by the schema \u25a1(\u25a1 <jats:italic>A<\/jats:italic> \u2192 <jats:italic>A<\/jats:italic>) \u2192 \u25a1 <jats:italic>A<\/jats:italic>, and <jats:italic>Grz<\/jats:italic> is the extension of <jats:italic>S<\/jats:italic><jats:sub>4<\/jats:sub> by \u25a1(\u25a1(<jats:italic>A<\/jats:italic> \u2192 \u25a1<jats:italic>A<\/jats:italic>) \u2192<jats:italic>A<\/jats:italic>) \u2192 \u25a1<jats:italic>A<\/jats:italic>. <jats:italic>GL<\/jats:italic> is also known to be sound and complete with respect to the class of all Kripke models that are transitive, irreflexive and well founded. <jats:italic>Grz<\/jats:italic> bears the same relation to the corresponding reflexive models. We refer the reader to [1] for a full exposition of the subject. (See also [4], [2], [6].)<\/jats:p><jats:p>In \u00a7I we develop a sequential calculus for both <jats:italic>GL<\/jats:italic> and <jats:italic>Grz<\/jats:italic> and give a semantical proof that both systems admit cut-elimination. (Incidentally, this provides an easy proof of the semantical completeness of the two systems.) With respect to <jats:italic>GL<\/jats:italic> this yields a correction of an error in [2].<\/jats:p><jats:p>In \u00a7II we show that cut-elimination fails for <jats:italic>QGL<\/jats:italic> (the extension of <jats:italic>GL<\/jats:italic> to a language with quantifiers). We further show that, despite this failure, <jats:italic>QGL<\/jats:italic> still has some of <jats:italic>GL'<\/jats:italic>s interesting properties (e.g., the disjunction property). We also show, using fixed-point techniques, that similar properties obtain if we take as semantics for <jats:italic>QGL<\/jats:italic> the arithmetical interpretation extended in the obvious way.<\/jats:p><jats:p>We want to thank Professor H. Gaifman for his help while working on the subject.<\/jats:p>","DOI":"10.2307\/2274147","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:09:38Z","timestamp":1146953378000},"page":"935-942","source":"Crossref","is-referenced-by-count":34,"title":["On modal systems having arithmetical interpretations"],"prefix":"10.1017","volume":"49","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200043085_ref010","unstructured":"Visser A. , On the provability logic of any recursive enumerable extension of Peano arithmetic or another look at Solovay proof (to appear)."},{"key":"S0022481200043085_ref008","first-page":"115","article-title":"Arithmetically complete modal theories","volume":"14","author":"Art\u00e9mov","year":"1980","journal-title":"S\u00e9miotika i Informatika"},{"key":"S0022481200043085_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757006"},{"key":"S0022481200043085_ref003","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883515"},{"key":"S0022481200043085_ref002","first-page":"531","volume":"46","author":"Leviant","year":"1981","journal-title":"On the proof theory of the modal logic for arithmetic provability"},{"key":"S0022481200043085_ref001","volume-title":"The unprovability of consistency","author":"Boolos","year":"1979"},{"key":"S0022481200043085_ref007","first-page":"191","volume":"47","author":"Boolos","year":"1982","journal-title":"Extremely undecidable sentences"},{"key":"S0022481200043085_ref005","volume-title":"Proof theory","author":"Takeuti","year":"1978"},{"key":"S0022481200043085_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370323"},{"key":"S0022481200043085_ref009","first-page":"795","article-title":"On the diagonalizable algebra of Peano arithmetic","volume":"16","author":"Montagna","year":"1979","journal-title":"Unione Matematica Italiana: Bolletino B"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200043085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T19:48:58Z","timestamp":1558640938000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200043085\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984,9]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1984,9]]}},"alternative-id":["S0022481200043085"],"URL":"https:\/\/doi.org\/10.2307\/2274147","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1984,9]]}}}