{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T04:55:41Z","timestamp":1648529741995},"reference-count":13,"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":14437,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1974,9]]},"abstract":"<jats:p>In this paper we show the finite controllability of the Maslov class of formulas of pure quantification theory (specified immediately below). That is, we show that every formula in the class has a finite model if it has a model at all. A <jats:italic>signed atomic formula<\/jats:italic> is an atomic formula or the negation of one; a <jats:italic>binary disjunction<\/jats:italic> is a disjunction of the form <jats:italic>A<\/jats:italic><jats:sub>1<\/jats:sub> \u22c1 <jats:italic>A<\/jats:italic><jats:sub>2<\/jats:sub>, where <jats:italic>A<\/jats:italic><jats:sub>1<\/jats:sub> and <jats:italic>A<\/jats:italic><jats:sub>2<\/jats:sub> are signed atomic formulas; and a formula is <jats:italic>Krom<\/jats:italic> if it is a conjunction of binary disjunctions. Finally, a prenex formula is <jats:italic>Maslov<\/jats:italic> if its prefix is \u2203\u00b7\u00b7\u00b7\u2203\u2200\u00b7\u00b7\u00b7\u2200\u2203\u00b7\u00b7\u00b7\u2203 and its matrix is Krom.<\/jats:p><jats:p>A number of decidability results have been obtained for formulas classified along these lines. It is a consequence of Theorems 1.7 and 2.5 of [4] that the following are reduction classes (for satisfiability): the class of Skolem formulas, that is, prenex formulas with prefixes \u2200\u00b7\u00b7\u00b7\u2200\u2203\u00b7\u00b7\u00b7\u2203, whose matrices are conjunctions one conjunct of which is a ternary disjunction and the rest of which are binary disjunctions; and the class of Skolem formulas containing identity whose matrices are Krom. Moreover, the following results (for pure quantification theory, that is, without identity) are derived in [1] and [2]: the classes of prenex formulas with Krom matrices and prefixes \u2203\u2200\u2203\u2200, or prefixes \u2200\u2203\u2203\u2200, or prefixes \u2200\u2203\u2200\u2200 are all reduction classes, while formulas with Krom matrices and prefixes \u2200\u2203\u2200 comprise a decidable class. The latter class, however, is not finitely controllable, for it contains formulas satisfiable only over infinite universes. The Maslov class was shown decidable by Maslov in [11].<\/jats:p>","DOI":"10.2307\/2272893","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:31:33Z","timestamp":1146951093000},"page":"509-518","source":"Crossref","is-referenced-by-count":1,"title":["The finite controllability of the Maslov case"],"prefix":"10.1017","volume":"39","author":[{"given":"St\u00e5l","family":"Aanderaa","sequence":"first","affiliation":[]},{"given":"Warren D.","family":"Goldfarb","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200076660_ref007","doi-asserted-by":"publisher","DOI":"10.2307\/3613396"},{"key":"S0022481200076660_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BF01452848"},{"key":"S0022481200076660_ref001","first-page":"4\u201314","volume-title":"Proceedings of the second Scandinavian logic symposium","author":"Aanderaa","year":"1971"},{"key":"S0022481200076660_ref002","first-page":"628\u2013642","volume":"38","author":"Aanderaa","year":"1973","journal-title":"Prefix classes of Krom formulas"},{"key":"S0022481200076660_ref004","first-page":"317\u2013326","volume":"27","author":"Chang","year":"1962","journal-title":"An improved prenex normal form"},{"key":"S0022481200076660_ref003","volume-title":"Solvable cases of the decision problem","author":"Ackermann","year":"1954"},{"key":"S0022481200076660_ref005","first-page":"32\u201347","volume-title":"Proceedings of a Harvard symposium on digital computers and their applications, 3\u20136 April 1961","author":"Dreben","year":"1962"},{"key":"S0022481200076660_ref006","unstructured":"Dreben B. and Goldfarb W. D. , A systematic treatment of the decision problem (to appear)."},{"key":"S0022481200076660_ref008","first-page":"27\u201328","article-title":"Ein Spezialfall des Entscheidungsproblems der theoretischen Logik","volume":"2","author":"G\u00f6del","year":"1932","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"S0022481200076660_ref009","first-page":"433\u2013443","article-title":"Zum Entscheidungsproblem des logischen Funktionenkalk\u00fcls","volume":"40","author":"G\u00f6del","year":"1933","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"S0022481200076660_ref011","first-page":"1420\u20131424","article-title":"An inverse method of establishing deducibilities in the classical predicate calculus","volume":"5","author":"Maslov","year":"1964","journal-title":"Soviet Mathematics\u2014Doklady"},{"key":"S0022481200076660_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449155"},{"key":"S0022481200076660_ref013","first-page":"161\u2013194","article-title":"\u00dcber die Erf\u00fcllbarkeit einer Klasse von logischen Formeln","volume":"110","author":"Sch\u00fctte","year":"1934","journal-title":"Mathematische Annalen"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200076660","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T21:03:33Z","timestamp":1559163813000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200076660\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1974,9]]},"references-count":13,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1974,9]]}},"alternative-id":["S0022481200076660"],"URL":"https:\/\/doi.org\/10.2307\/2272893","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1974,9]]}}}