{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:35Z","timestamp":1783111475533,"version":"3.54.6"},"reference-count":19,"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":8593,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>PA is Peano arithmetic. The formula Interp<jats:sub>PA<\/jats:sub>(\u03b1, \u03b2) is a formalization of the assertion that the theory PA + \u03b1 interprets the theory PA + \u03b2 (the variables \u03b1 and \u03b2 are intended to range over codes of sentences of PA). We extend Solovay's modal analysis of the formalized provability predicate of PA, Pr<jats:sub>PA<\/jats:sub>(<jats:italic>x<\/jats:italic>), to the case of the formalized interpretability relation Interp<jats:sub>PA<\/jats:sub>(<jats:italic>x, y<\/jats:italic>). The relevant modal logic, in addition to the usual provability operator \u2018\u25a1\u2019, has a binary operator \u2018\u22b3\u2019 to be interpreted as the formalized interpretability relation. We give an axiomatization and a decision procedure for the class of those modal formulas that express valid interpretability principles (for every assignment of the atomic modal formulas to sentences of PA). Our results continue to hold if we replace the base theory PA with Zermelo-Fraenkel set theory, but not with G\u00f6del-Bernays set theory. This sensitivity to the base theory shows that the language is quite expressive. Our proof uses in an essential way earlier work done by A. Visser, D. de Jongh, and F. Veltman on this problem.<\/jats:p>","DOI":"10.2307\/2274474","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:36:50Z","timestamp":1146955010000},"page":"1059-1089","source":"Crossref","is-referenced-by-count":52,"title":["The interpretability logic of Peano arithmetic"],"prefix":"10.1017","volume":"55","author":[{"given":"Alessandro","family":"Berarducci","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200025561_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8601-8"},{"key":"S0022481200025561_ref014","first-page":"212","volume-title":"Harvey Friedman's research on the foundations of mathematics","author":"Smory\u0144ski","year":"1985"},{"key":"S0022481200025561_ref001","first-page":"270","article-title":"Nonarithmeticity of truth predicate logics of provability","volume":"284","author":"Artemov","year":"1985","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200025561_ref004","volume-title":"The unprovability of consistency","author":"Boolos","year":"1979"},{"key":"S0022481200025561_ref008","first-page":"329","volume-title":"Proceedings from 5th Scandinavian logic symposium","author":"Lindstr\u00f6m","year":"1979"},{"key":"S0022481200025561_ref018","volume-title":"Preliminary notes on interpretability logic","author":"Visser","year":"1988"},{"key":"S0022481200025561_ref002","unstructured":"Berarducci Alessandro , The interpretability logic of Peano arithmetic (preliminary version), Manuscript, 1988."},{"key":"S0022481200025561_ref011","first-page":"423","volume":"50","author":"Pudl\u00e1k","year":"1985","journal-title":"Cuts, consistency statements and interpretability"},{"key":"S0022481200025561_ref017","first-page":"11","article-title":"Arithmetic complexity of predicate logics of provability and their fragments","volume":"288","author":"Vardanyan","year":"1986","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200025561_ref010","first-page":"45","volume-title":"Infinitistic methods (proceedings of the symposium on foundations of mathematics, Warsaw, 1959)","author":"Montague","year":"1961"},{"key":"S0022481200025561_ref007","unstructured":"Friedman Harvey , Translatability and relative consistency. II, manuscript."},{"key":"S0022481200025561_ref003","first-page":"177","article-title":"\u03a3n0 interpretations of modal logic","volume":"3","author":"Berarducci","year":"1989","journal-title":"Bollettino dell'Unione Matematica Italiana"},{"key":"S0022481200025561_ref005","volume-title":"Proceedings of Heyting '88","author":"de Jongh"},{"key":"S0022481200025561_ref006","doi-asserted-by":"publisher","DOI":"10.4064\/fm-49-1-35-92"},{"key":"S0022481200025561_ref009","first-page":"431","volume-title":"Atti degli incontri di logica matematica (Siena, 1983, 1984","volume":"2","author":"Lindstr\u00f6m","year":"1985"},{"key":"S0022481200025561_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"S0022481200025561_ref013","volume-title":"Logic of relative interpretability over Peano arithmetic","author":"Shavrukov","year":"1988"},{"key":"S0022481200025561_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757006"},{"key":"S0022481200025561_ref019","volume-title":"Interpretability logic","author":"Visser","year":"1988"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200025561","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T20:25:18Z","timestamp":1558211118000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200025561\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,9]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1990,9]]}},"alternative-id":["S0022481200025561"],"URL":"https:\/\/doi.org\/10.2307\/2274474","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,9]]}}}