{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T17:35:53Z","timestamp":1648748153714},"reference-count":6,"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":10054,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1986,9]]},"abstract":"<jats:p>Fred Richman conjectured that the following principle is not constructive:<\/jats:p><jats:p>(*) If <jats:italic>A<\/jats:italic> is a decidable subset of the set N of natural numbers and if, for every decidable subset <jats:italic>B<\/jats:italic> of N, either <jats:italic>A<\/jats:italic> \u2286 <jats:italic>B<\/jats:italic> or <jats:italic>A<\/jats:italic> \u2286 N \u2212 <jats:italic>B<\/jats:italic>, then, for some <jats:italic>n<\/jats:italic> \u2208 N, <jats:italic>A<\/jats:italic> \u2286 {<jats:italic>n<\/jats:italic>}.<\/jats:p><jats:p><jats:disp-quote><jats:p>A set <jats:italic>A<\/jats:italic> of natural numbers is called decidable if \u2200<jats:italic>n<\/jats:italic>(<jats:italic>n<\/jats:italic> \u2208 <jats:italic>A<\/jats:italic> \u2228 \u2309 (<jats:italic>n<\/jats:italic> \u2208 <jats:italic>A<\/jats:italic>)) holds. In recursive models, this agrees with the recursion-theoretic meaning of decidability. In other contexts, \u201ccomplemented\u201d and \u201cdetachable\u201d are often used.<\/jats:p><\/jats:disp-quote><\/jats:p><jats:p>Richman's conjecture was motivated by the problem of uniqueness of divisible hulls of abelian groups in constructive algebra. Richman showed that a countable discrete abelian <jats:italic>p<\/jats:italic>-group <jats:italic>G<\/jats:italic> has a unique (up to isomorphism over <jats:italic>G<\/jats:italic>) divisible hull if the subgroup <jats:italic>pG<\/jats:italic> is decidable. He also showed that the converse implies.<\/jats:p><jats:p>We confirm the nonconstructive nature of by showing (in \u00a71) that it is not provable in intuitionistic set theory, IZF. Thus, in the models we construct, there are countable discrete abelian <jats:italic>p<\/jats:italic>-groups <jats:italic>G<\/jats:italic> whose divisible hulls are unique but whose subgroups <jats:italic>pG<\/jats:italic> are not decidable.<\/jats:p><jats:p>Our models do not satisfy further conditions imposed by Richman, namely Church's Thesis and Markov's Principle, so the full conjecture remains an open problem. We do, however, show (in \u00a72) how to embellish our first model so that the fan theorem (i.e., compactness of 2<jats:sup>N<\/jats:sup>) fails. (Church's Thesis implies the stronger statement that the negation of the fan theorem holds.)<\/jats:p><jats:p>Our models will be constructed by the method of sheaf semantics [1], [3]. That is, we shall construct Grothendieck topoi in whose internal logic fails.<\/jats:p>","DOI":"10.2307\/2274026","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:18:32Z","timestamp":1146953912000},"page":"726-731","source":"Crossref","is-referenced-by-count":2,"title":["Small decidable sheaves"],"prefix":"10.1017","volume":"51","author":[{"given":"Andreas","family":"Blass","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200030899_ref006","first-page":"194","article-title":"Extending the topological interpretation to intuitionistic analysis","volume":"20","author":"Scott","year":"1968","journal-title":"Compositio Mathematica"},{"key":"S0022481200030899_ref005","first-page":"435","volume-title":"The L. E. J. Brouwer Centenary Symposium","author":"Scedrov","year":"1982"},{"key":"S0022481200030899_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(80)90096-1"},{"key":"S0022481200030899_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061824"},{"key":"S0022481200030899_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061823"},{"key":"S0022481200030899_ref001","first-page":"6","volume":"46","author":"Boileau","year":"1981","journal-title":"La logique des topos"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200030899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T04:40:46Z","timestamp":1558500046000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200030899\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,9]]},"references-count":6,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1986,9]]}},"alternative-id":["S0022481200030899"],"URL":"https:\/\/doi.org\/10.2307\/2274026","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986,9]]}}}