{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T16:52:55Z","timestamp":1778691175830,"version":"3.51.4"},"reference-count":11,"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":15990,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1970,6]]},"abstract":"<jats:p>In [8] S. J. Maslov gives a positive solution to the decision problem for satisfiability of formulas of the form<\/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=\"S0022481200090861_eqnU1\"\/><\/jats:disp-formula><\/jats:p><jats:p>in any first-order predicate calculus without identity where <jats:italic>h, k, m, n<\/jats:italic> are positive integers, <jats:italic>\u03b1<jats:sub>i<\/jats:sub>, \u03b2<jats:sub>i<\/jats:sub><\/jats:italic> are signed atomic formulas (atomic formulas or negations of atomic formulas), and \u2227, \u2228 are conjunction and disjunction symbols, respectively (cf. [6] for a related solvable class). In this paper we show that the decision problem is unsolvable for formulas that are like those considered by Maslov except that they have prefixes of the form \u2200<jats:italic>x<\/jats:italic>\u2203<jats:italic>y<\/jats:italic><jats:sub>1<\/jats:sub> \u2026 \u2203<jats:italic>y<jats:sub>k<\/jats:sub><\/jats:italic>\u2200<jats:italic>z<\/jats:italic>. This settles the decision problems for all prefix classes of formulas for formulas that are in prenex conjunctive normal form in which all disjunctions are binary (have just two terms). In our concluding section we report results on decision problems for related classes of formulas including classes of formulas in languages with identity and we describe some special properties of formulas in which all disjunctions are binary including a property that implies that any proof of our result, that a class of formulas is a reduction class for satisfiability, is necessarily indirect. Our proof is based on an unsolvable combinatorial tag problem.<\/jats:p>","DOI":"10.2307\/2270511","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:00:41Z","timestamp":1146934841000},"page":"210-216","source":"Crossref","is-referenced-by-count":14,"title":["The decision problem for formulas in prenex conjunctive normal form with binary disjunctions"],"prefix":"10.1017","volume":"35","author":[{"given":"M. R.","family":"Krom","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200090861_ref005","first-page":"403","article-title":"Some interpolation theorems for first-order formulas in which all disjunctions are binary","volume":"43","author":"Krom","year":"1968","journal-title":"Logique et analyse"},{"key":"S0022481200090861_ref003","first-page":"12","article-title":"Sur le probl\u00e8me fondamental de la logique math\u00e9matique","volume":"24","author":"Herbrand","year":"1931","journal-title":"Comptes Rendus des S\u00e9ances de la Soci\u00e9t\u00e9 des Sciences et des Lettres de Varsovie Classe"},{"key":"S0022481200090861_ref009","volume-title":"Introduction to model theory and to the metamathematics of algebra","author":"Robinson","year":"1963"},{"key":"S0022481200090861_ref008","first-page":"1420","article-title":"An inverse method of establishing deducibilities in the classical predicate calculus","volume":"159","author":"Maslov","year":"1964","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200090861_ref007","doi-asserted-by":"publisher","DOI":"10.7146\/math.scand.a-10862"},{"key":"S0022481200090861_ref004","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093958753"},{"key":"S0022481200090861_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF01343730"},{"key":"S0022481200090861_ref006","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19670130104"},{"key":"S0022481200090861_ref001","first-page":"317","article-title":"An improved prenex normal form","volume":"27","author":"Chang","year":"1962","journal-title":"this Journal"},{"key":"S0022481200090861_ref002","doi-asserted-by":"publisher","DOI":"10.1145\/321203.321206"},{"key":"S0022481200090861_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70304-0"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200090861","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T15:12:22Z","timestamp":1559401942000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200090861\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1970,6]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1970,6]]}},"alternative-id":["S0022481200090861"],"URL":"https:\/\/doi.org\/10.2307\/2270511","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1970,6]]}}}