{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:13:34Z","timestamp":1776888814545,"version":"3.51.2"},"reference-count":7,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":9873,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1987,3]]},"abstract":"<jats:p>The formalism of P(redicate) P(rovability) L(ogic) is the result of adjoining the unary operator \u25a1 to first-order logic without identity, constants, or function symbols. The term \u201cprovability\u201d indicates that \u25a1 is to be \u201cread\u201d as \u201cit is provable in P(eano) A(rithmetic) that\u2026\u201d and that the formulae of predicate provability logic are to be interpreted via formulae of PA as follows.<\/jats:p><jats:p>Pr(<jats:italic>x<\/jats:italic>), alias Bew(<jats:italic>x<\/jats:italic>), is the standard provability predicate of PA. For any formula <jats:italic>F<\/jats:italic> of PA, Pr[<jats:italic>F<\/jats:italic>] is the formula of PA that expresses the PA-provability of <jats:italic>F<\/jats:italic> \u201cof\u201d the values of the variables free in <jats:italic>F<\/jats:italic>, i.e., it is the formula of PA with the same free variables as <jats:italic>F<\/jats:italic> that expresses the PA-provability of the result of substituting for each variable free in <jats:italic>F<\/jats:italic> the numeral for the value of that variable. For the details of the construction of Pr[<jats:italic>F<\/jats:italic>], the reader may consult [B2, p. 42]. If <jats:italic>F<\/jats:italic> is a <jats:italic>sentence<\/jats:italic> of PA, then Pr[<jats:italic>F<\/jats:italic>] = Pr(\u2018<jats:italic>F<\/jats:italic>\u2019), the sentence that expresses the PA-provability of <jats:italic>F<\/jats:italic>.<\/jats:p><jats:p>Let <jats:italic>\u03c5<\/jats:italic><jats:sub>1<\/jats:sub>, <jats:italic>\u03c5<\/jats:italic><jats:sub>2<\/jats:sub>,\u2026 be an enumeration of the variables of PA. An <jats:italic>interpretation<\/jats:italic> * of a formula <jats:italic>\u03d5<\/jats:italic> of PPL is a function which assigns to each predicate symbol <jats:italic>P<\/jats:italic> of <jats:italic>\u03d5<\/jats:italic> a formula <jats:italic>P<\/jats:italic>* of the language of arithmetic whose free variables are the first <jats:italic>n<\/jats:italic> variables of PA, where <jats:italic>n<\/jats:italic> is the degree of <jats:italic>P<\/jats:italic>.<\/jats:p>","DOI":"10.2307\/2273871","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:20:33Z","timestamp":1146954033000},"page":"165-171","source":"Crossref","is-referenced-by-count":8,"title":["The degree of the set of sentences of predicate provability logic that are true under every interpretation"],"prefix":"10.1017","volume":"52","author":[{"given":"George","family":"Boolos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vann","family":"McGee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200030085_bib006","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757006"},{"key":"S0022481200030085_bib003","volume-title":"The unprovability of consistency","author":"Boolos","year":"1979"},{"key":"S0022481200030085_bib005","first-page":"113","volume":"40","author":"Friedman","year":"1975","journal-title":"One hundred and two problems in mathematical logic"},{"key":"S0022481200030085_bib007","volume-title":"O predikatno\u012d logike dokazuemosti","author":"Vardanyan","year":"1985"},{"key":"S0022481200030085_bib004","volume-title":"Computability and unsolvability","author":"Davis","year":"1958"},{"key":"S0022481200030085_bib002","first-page":"779","volume":"41","author":"Boolos","year":"1976","journal-title":"On deciding the truth of certain statements involving the notion of consistency"},{"key":"S0022481200030085_bib001","first-page":"270","article-title":"Nonarithmeticity of truth predicate logics of provability","volume":"284","author":"Artemov","year":"1985","journal-title":"Doklady Akademii Nauk SSSR"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200030085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T08:12:22Z","timestamp":1649664742000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200030085\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,3]]},"references-count":7,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1987,3]]}},"alternative-id":["S0022481200030085"],"URL":"https:\/\/doi.org\/10.2307\/2273871","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,3]]}}}