{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:16:31Z","timestamp":1754396191185},"reference-count":8,"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":14894,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1973,6]]},"abstract":"<jats:p>Let <jats:italic>U<\/jats:italic> be a consistent axiomatic theory containing Robinson's <jats:italic>Q<\/jats:italic> [TMRUT, p. 51]. In order for the results below to be of interest, <jats:italic>U<\/jats:italic> must be powerful enough to carry out certain arguments involving versions of the \u201cderivability conditions,\u201d DC(i) to DC(iii) below, of [HBGM, p. 285], [F60, Theorem 4.7], or [L55]. Thus it must contain, at least, mathematical induction for formulas whose prenex normal forms contain at most existential quantifiers. For convenience, <jats:italic>U<\/jats:italic> is assumed also to contain symbols for primitive recursive functions and relations, and their defining equations. One of these is used to form the standard provability predicate, Prov \u02f9<jats:italic>A<\/jats:italic>\u02fa, \u201cthere exists a number which is the G\u00f6del number of a proof of <jats:italic>A<\/jats:italic>.\u201d Upper corners denote numerals for G\u00f6del numbers for the enclosed sentences, and parentheses are often omitted in their presence.<\/jats:p><jats:p>This paper contains some results concerning the relation between the sentence <jats:italic>A<\/jats:italic>, and the sentence Prov \u02f9<jats:italic>A<\/jats:italic>\u02fa in the Lindenbaum Sentence Algebra (LSA) for <jats:italic>U<\/jats:italic>, the Boolean algebra induced by the pre-order relation <jats:italic>A \u2264 B \u21d4 \u22a6A \u2192 B<\/jats:italic>. Half of the answer is provided by a theorem of L\u00f6b [L55], which states that \u22a6Prov \u02f9<jats:italic>A<\/jats:italic>\u02fa \u2192 <jats:italic>A<\/jats:italic> \u21d4 \u22a6<jats:italic>A<\/jats:italic>. Hence, in the presence of DC(iii), below, it is never true that Prov \u02f9<jats:italic>A<\/jats:italic>\u02fa &lt; <jats:italic>A<\/jats:italic> in the LSA. However, there is a large and interesting set of sentences, denoted here by \u0393, for which <jats:italic>A<\/jats:italic> &lt; Prov \u231c<jats:italic>A<\/jats:italic>\u231d.<\/jats:p>","DOI":"10.2307\/2272065","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:22:43Z","timestamp":1146950563000},"page":"295-298","source":"Crossref","is-referenced-by-count":11,"title":["The relation of <i>A<\/i> to Prov \u02f9<i>A<\/i>\u02fa in the Lindenbaum sentence algebra"],"prefix":"10.1017","volume":"38","author":[{"given":"C. F.","family":"Kent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200077896_ref003","volume-title":"Grundlagen der Mathematik","author":"Hilbert","year":"1939"},{"key":"S0022481200077896_ref007","volume-title":"Beweistheorie","author":"Sch\u00fctte","year":"1960"},{"key":"S0022481200077896_ref008","volume-title":"Undecldable theories","author":"Tarski","year":"1966"},{"key":"S0022481200077896_ref005","first-page":"115","volume":"20","author":"L\u00f6b","year":"1955","journal-title":"Solution of a problem of Leon Henkin"},{"key":"S0022481200077896_ref001","doi-asserted-by":"publisher","DOI":"10.4064\/fm-49-1-35-92"},{"key":"S0022481200077896_ref004","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19680140702"},{"key":"S0022481200077896_ref002","first-page":"259","volume":"27","author":"Feferman","year":"1962","journal-title":"Transfinite recursive progressions of axiomatic theories"},{"key":"S0022481200077896_ref006","volume-title":"Theory of recursive functions and effective computability","author":"Rogers","year":"1967"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200077896","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:54:23Z","timestamp":1559246063000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200077896\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1973,6]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1973,6]]}},"alternative-id":["S0022481200077896"],"URL":"https:\/\/doi.org\/10.2307\/2272065","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1973,6]]}}}