{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T04:01:00Z","timestamp":1648958460207},"reference-count":4,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13433,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1977,6]]},"abstract":"Terminology<\/jats:italic>. PA is Peano Arithmetic, classical first-order arithmetic with induction. \u2308A<\/jats:italic>\u2309 is the formal numeral in PA for the G\u00f6del number of A<\/jats:italic>. \u2013 A<\/jats:italic> is the negation of A<\/jats:italic>, (A&B<\/jats:italic>) is the conjunction of A<\/jats:italic> and B<\/jats:italic>, and Bew(x<\/jats:italic>) is the usual provability predicate for PA. neg(x<\/jats:italic>), conj(x, y<\/jats:italic>), bicond(x, y<\/jats:italic>), and bew(x<\/jats:italic>) are terms of PA such that for all sentences A<\/jats:italic> and B<\/jats:italic> of PA \u22a2PA<\/jats:sub>, neg(\u02f9A<\/jats:italic>\u02fa) = \u02f9\u2212A<\/jats:italic>\u02fa \u22a2PA<\/jats:sub> Conj(\u02f9A<\/jats:italic>\u02fa, \u02f9B<\/jats:italic>\u02fa)= \u02f9(A&B<\/jats:italic>)\u02fa \u22a2PA<\/jats:sub> bicond(\u02f9A<\/jats:italic>\u02fa, \u02f9B<\/jats:italic>\u02fa)= \u02f9(A<\/jats:italic> \u2194 B<\/jats:italic>)\u02fa, and \u22a2PA<\/jats:sub> bew(\u02f9A<\/jats:italic>\u02fa) = \u02f9Bew(\u02f9A<\/jats:italic>\u02fa)\u02fa. T<\/jats:italic> is the sentence \u20180 = 0\u2019 and Con is the usual sentence expressing the consistency of PA. If A (x)<\/jats:italic> is any formula of PA, then a fixed point of A(x)<\/jats:italic> is a sentence S<\/jats:italic> such that \u22a2PA<\/jats:italic><\/jats:sub>S<\/jats:italic> \u2194 A<\/jats:italic>(\u02f9S<\/jats:italic>\u02fa). (It is well known that every formula of PA with one free variable has a fixed point.) The P-terms<\/jats:italic> are defined inductively by: the variable x<\/jats:italic> is a P<\/jats:italic>-term; if t(x)<\/jats:italic> and u(x)<\/jats:italic> are P<\/jats:italic>-terms, so are neg(t(x))<\/jats:italic>, conj(t(x), u(x))<\/jats:italic>, and bew(t(x)<\/jats:italic>). A basic P-formula<\/jats:italic> is a formula Bew(t(x))<\/jats:italic>, where t(x)<\/jats:italic> is a P<\/jats:italic>-term; and a P-formula<\/jats:italic> is a truth-functional combination of basic P<\/jats:italic>-formulas. An F-sentence<\/jats:italic> is a member of the smallest class that contains Con and contains \u2212A<\/jats:italic>, (A&B<\/jats:italic>), and \u2212Bew(\u02f9\u2212A\u02fa) whenever it contains A<\/jats:italic> and B<\/jats:italic>. In [B] we gave a decision procedure for the class of true F<\/jats:italic>-sentences.<\/jats:p>\u2212Bew(x<\/jats:italic>), Bew(x<\/jats:italic>), and Bew(neg(x<\/jats:italic>)) are examples of P<\/jats:italic>-formulas, and fixed points of these particular P<\/jats:italic>-formulas have been studied by G\u00f6del, Henkin [H] and L\u00f6b [L], and Jeroslow [J], respectively. In this note we show how to decide whether or not a fixed point of any given P<\/jats:italic>-formula is provable in PA.<\/jats:p>","DOI":"10.2307\/2272119","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:44:08Z","timestamp":1146951848000},"page":"191-193","source":"Crossref","is-referenced-by-count":0,"title":["On deciding the provability of certain fixed point statements"],"prefix":"10.1017","volume":"42","author":[{"given":"George","family":"Boolos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200050350_ref002","first-page":"160","volume":"17","author":"Henkin","year":"1952","journal-title":"A problem concerning provability"},{"key":"S0022481200050350_ref004","first-page":"115","volume":"20","author":"L\u00f6b","year":"1955","journal-title":"Solution of a problem of Leon Henkin"},{"key":"S0022481200050350_ref001","first-page":"779","volume":"41","author":"Boolos","year":"1976","journal-title":"On deciding the truth of certain statements involving the notion of consistency"},{"key":"S0022481200050350_ref003","first-page":"359","volume":"38","author":"Jeroslow","year":"1973","journal-title":"Redundancies in the Hilbert-Bernays derivability conditions for G\u00f6del's second incompleteness theorem"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200050350","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T21:35:09Z","timestamp":1558992909000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200050350\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1977,6]]},"references-count":4,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1977,6]]}},"alternative-id":["S0022481200050350"],"URL":"https:\/\/doi.org\/10.2307\/2272119","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1977,6]]}}}