{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T22:22:48Z","timestamp":1648592568686},"reference-count":9,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":14256,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1975,3]]},"abstract":"Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form \u2200\u00b7\u00b7\u00b7\u2200\u2203\u00b7\u00b7\u00b7\u2203 is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the \u2200\u2200\u2200\u2203 class is a reduction class, for G\u00f6del [3], Kalm\u00e1r [4], and Sch\u00fctte [6] showed the \u2200\u2200\u2203\u00b7\u00b7\u00b7\u2203 class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.<\/jats:p>Let x<\/jats:italic>, y<\/jats:italic>1<\/jats:sub>, y<\/jats:italic>2<\/jats:sub>, be distinct variables (we shall use v<\/jats:italic>1<\/jats:sub>, v<\/jats:italic>2<\/jats:sub>, \u00b7\u00b7\u00b7 and w<\/jats:italic>1<\/jats:sub>, w<\/jats:italic>2<\/jats:sub>, \u00b7\u00b7\u00b7 as metavariables ranging over these variables), and for each i<\/jats:italic> \u2265 1 let Y<\/jats:italic>(i<\/jats:italic>)<\/jats:sup> be the set {y<\/jats:italic>1<\/jats:sub>, \u00b7\u00b7\u00b7, y<\/jats:italic>i<\/jats:sub>}. An atomic formula Pv<\/jats:italic>1<\/jats:sub> \u00b7\u00b7\u00b7 v<\/jats:italic>k<\/jats:sub> will be said to be {v<\/jats:italic>1<\/jats:sub>, \u00b7\u00b7\u00b7, v<\/jats:italic>k<\/jats:sub>}-based<\/jats:italic>. For any n<\/jats:italic> \u2265 1, p<\/jats:italic> \u2265 1, and any subsets Y<\/jats:italic>1<\/jats:sub>, \u00b7\u00b7\u00b7 Y<\/jats:italic>p<\/jats:sub> of Y<\/jats:italic>(n<\/jats:italic>)<\/jats:sup>, let C<\/jats:italic>(n<\/jats:italic>, Y<\/jats:italic>1<\/jats:sub>, \u00b7\u00b7\u00b7, Yp<\/jats:sub><\/jats:italic>) be the class of all those closed formulas with prefix \u2200y<\/jats:italic>1<\/jats:sub> \u00b7\u00b7\u00b7 \u2200yn<\/jats:sub><\/jats:italic>\u2203x<\/jats:italic> such that each atomic subformula not containing the variable x<\/jats:italic> is Yi<\/jats:sub><\/jats:italic>-based for some i<\/jats:italic>, 1 \u2264 i<\/jats:italic> \u2264 p<\/jats:italic>.<\/jats:p>","DOI":"10.2307\/2272272","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:33:55Z","timestamp":1146936835000},"page":"62-68","source":"Crossref","is-referenced-by-count":1,"title":["Skolem reduction classes"],"prefix":"10.1017","volume":"40","author":[{"given":"Warren D.","family":"Goldfarb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harry R.","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200054281_ref009","volume-title":"Proceedings of a symposium on the mathematical theory of automata","author":"Wang","year":"1962"},{"key":"S0022481200054281_ref007","volume-title":"Videnskapsselskapets Skrifter, Mat.-Naturv. Klasse 4","author":"Skolem","year":"1920"},{"key":"S0022481200054281_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01452848"},{"key":"S0022481200054281_ref003","first-page":"27","article-title":"Ein Spezialfall des Entscheidungsproblems der theoretischen Logik","volume":"2","author":"G\u00f6del","year":"1932","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"S0022481200054281_ref002","unstructured":"Dreben B. and Goldfarb W. D. , A systematic treatment of the decision problem (in preparation)."},{"key":"S0022481200054281_ref005","volume-title":"Formal'naia logika i metodologiia nauki","author":"Makanin","year":"1964"},{"key":"S0022481200054281_ref001","volume-title":"Memoirs of the American Mathematical Society","author":"Berger","year":"1966"},{"key":"S0022481200054281_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF02021316"},{"key":"S0022481200054281_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449155"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200054281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T16:05:44Z","timestamp":1559145944000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200054281\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1975,3]]},"references-count":9,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1975,3]]}},"alternative-id":["S0022481200054281"],"URL":"https:\/\/doi.org\/10.2307\/2272272","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1975,3]]}}}