{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:18Z","timestamp":1761611178227},"reference-count":3,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13615,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1976,12]]},"abstract":"<jats:p>Friedman has posed (see [F, p. 117]) the following problem: \u201c35. Define the set <jats:italic>E<\/jats:italic> of expressions by (i) Con is an expression; (ii) if <jats:italic>A, B<\/jats:italic> are expressions so are (~ <jats:italic>A<\/jats:italic>), (<jats:italic>A&amp;B<\/jats:italic>), and Con(<jats:italic>A<\/jats:italic>). Each expression <jats:italic>\u03d5<\/jats:italic> in <jats:italic>E<\/jats:italic> determines a sentence \u03d5 in <jats:italic>PA<\/jats:italic> [classical first-order arithmetic] by taking Con* to be \u201c<jats:italic>PA<\/jats:italic> is consistent,\u201d ( ~ <jats:italic>A<\/jats:italic>) * to be ~ (<jats:italic>A<\/jats:italic>*), (<jats:italic>A&amp;B<\/jats:italic>)* to be <jats:italic>A<\/jats:italic>*&amp;<jats:italic>B<\/jats:italic>*, and Con(<jats:italic>A<\/jats:italic>)* to be \u201c<jats:italic>PA<\/jats:italic> + \u2018<jats:italic>A<\/jats:italic>*\u2019 is consistent.\u201d <jats:italic>The set of expressions \u03d5 \u2208 <jats:italic>E<\/jats:italic> such that \u03d5* is true is recursive<\/jats:italic>.<\/jats:p><jats:p>The formalized second incompleteness theorem reads<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200051008_eqnU1\" \/><\/jats:disp-formula><\/jats:p><jats:p>In order to simplify notation, we will reformulate Friedman's problem slightly. Let Con be the usual sentence of <jats:italic>PA<\/jats:italic> expressing the consistency of <jats:italic>PA<\/jats:italic>, ~ <jats:italic>A<\/jats:italic> the negation of <jats:italic>A<\/jats:italic>, (<jats:italic>A&amp;B<\/jats:italic>) the conjunction of <jats:italic>A<\/jats:italic> and <jats:italic>B<\/jats:italic>, etc., and Bew(<jats:italic>A<\/jats:italic>) the result of substituting the numeral for the G\u00f6del number of <jats:italic>A<\/jats:italic> for the free variable in the usual provability predicate for <jats:italic>PA<\/jats:italic>. Let Con(<jats:italic>A<\/jats:italic>) = ~ Bew(~ <jats:italic>A<\/jats:italic>). (Con(<jats:italic>A<\/jats:italic>) is equivalent in <jats:italic>PA<\/jats:italic> to the usual sentence expressing the consistency of <jats:italic>PA<\/jats:italic> + <jats:italic>A<\/jats:italic>.) And let the class of <jats:italic>F-sentences<\/jats:italic> be the smallest class which contains Con and which also contains ~ <jats:italic>A<\/jats:italic>, (<jats:italic>A&amp;B<\/jats:italic>) and Con(<jats:italic>A<\/jats:italic>) whenever it contains <jats:italic>A<\/jats:italic> and <jats:italic>B<\/jats:italic>. Since \u22a6<jats:sub><jats:italic>PA<\/jats:italic><\/jats:sub> Bew(<jats:italic>A<\/jats:italic>) \u2194 Bew(<jats:italic>B<\/jats:italic>) if \u22a6<jats:sub><jats:italic>PA<\/jats:italic><\/jats:sub><jats:italic>A<\/jats:italic> \u2194 <jats:italic>B<\/jats:italic>, Friedman's problem is then the question whether the class of true <jats:italic>F<\/jats:italic>-sentences is recursive.<\/jats:p><jats:p>The answer is that it is recursive. To see why, we need a definition and a theorem.<\/jats:p><jats:p>Definition. An <jats:italic>atom<\/jats:italic> is a sentence Con<jats:sup><jats:italic>n<\/jats:italic><\/jats:sup> for some <jats:italic>n<\/jats:italic> \u2265 1, where Con<jats:sup>t<\/jats:sup> = Con and Con<jats:sup><jats:italic>n<\/jats:italic> + 1<\/jats:sup> = Con(Con<jats:sup><jats:italic>n<\/jats:italic><\/jats:sup>).<\/jats:p>","DOI":"10.2307\/2272395","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:42:53Z","timestamp":1146951773000},"page":"779-781","source":"Crossref","is-referenced-by-count":9,"title":["On deciding the truth of certain statements involving the notion of consistency"],"prefix":"10.1017","volume":"41","author":[{"given":"George","family":"Boolos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200051008_ref003","first-page":"115","volume":"20","author":"L\u00f6b","year":"1955","journal-title":"Solution of a problem of Leon Henkin"},{"key":"S0022481200051008_ref001","volume-title":"Computability and logic","author":"Boolos","year":"1974"},{"key":"S0022481200051008_ref002","first-page":"113","volume":"40","author":"Friedman","year":"1975","journal-title":"One hundred and two problems in mathematical logic"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200051008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T19:47:04Z","timestamp":1559072824000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200051008\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,12]]},"references-count":3,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1976,12]]}},"alternative-id":["S0022481200051008"],"URL":"https:\/\/doi.org\/10.2307\/2272395","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1976,12]]}}}