{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T21:40:16Z","timestamp":1791409216584,"version":"4.3.3"},"reference-count":58,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":6164,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1997,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We identify the computational complexity of the satisfiability problem for FO<jats:sup>2<\/jats:sup>, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO<jats:sup>2<\/jats:sup> has the <jats:italic>finite-model property<\/jats:italic>, which means that if an FO<jats:sup>2<\/jats:sup>-sentence is satisiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO<jats:sub>2<\/jats:sub>-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO<jats:sup>2<\/jats:sup>-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO<jats:sup>2<\/jats:sup> is NEXPTIME-complete.<\/jats:p>","DOI":"10.2307\/421196","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:09:51Z","timestamp":1146985791000},"page":"53-69","source":"Crossref","is-referenced-by-count":194,"title":["On the Decision Problem for Two-Variable First-Order Logic"],"prefix":"10.1017","volume":"3","author":[{"given":"Erich","family":"Gr\u00e4del","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Phokion G.","family":"Kolaitis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600007666_ref051","volume-title":"Proceedings of the 12th international colloqium on automata, languages, and programming","volume":"104","author":"Reif","year":"1983"},{"key":"S1079898600007666_ref023","doi-asserted-by":"publisher","DOI":"10.2307\/2274274"},{"key":"S1079898600007666_ref055","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"S1079898600007666_ref032","volume-title":"Introduction to automata theory, languages and computation","author":"Hopcroft","year":"1979"},{"key":"S1079898600007666_ref021","first-page":"27","article-title":"Ein Spezialfall des Entscheidungsproblems der theoretischen Logik","volume":"2","author":"G\u00f6del","year":"1932","journal-title":"Ergebnisse der Mathematik Kolloq."},{"key":"S1079898600007666_ref014","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1084"},{"key":"S1079898600007666_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-4832-1453-5.50019-2"},{"key":"S1079898600007666_ref037","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90065-P"},{"key":"S1079898600007666_ref058","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"S1079898600007666_ref045","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"S1079898600007666_ref043","first-page":"374","volume-title":"Proceedings of the 6th international symposium on mathematical foundations of computer science","volume":"53","author":"Lipski","year":"1977"},{"key":"S1079898600007666_ref042","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"S1079898600007666_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305232"},{"key":"S1079898600007666_ref026","unstructured":"Gr\u00e4del E. , Otto M. , and Rosen E. , Two-variable logic with counting is decidable, unpublished manuscript, 1996."},{"key":"S1079898600007666_ref029","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"S1079898600007666_ref010","first-page":"280","volume-title":"Proceedings of the 8th international conference on very large data bases","author":"Castilho","year":"1982"},{"key":"S1079898600007666_ref053","first-page":"377","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott","year":"1962","journal-title":"Journal of Symbolic Logic"},{"key":"S1079898600007666_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90055-2"},{"key":"S1079898600007666_ref040","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"S1079898600007666_ref039","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1995.1055"},{"key":"S1079898600007666_ref054","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"S1079898600007666_ref016","volume-title":"K. G\u00f6del, collected works, volume I: Publications 1929\u20131936","author":"Feferman","year":"1986"},{"key":"S1079898600007666_ref050","first-page":"264","article-title":"On a problem in formal logic","volume":"30","author":"Ramsey","year":"1928","journal-title":"Proceedings of the London Mathematical Society"},{"key":"S1079898600007666_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01459101"},{"key":"S1079898600007666_ref049","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90061-6"},{"key":"S1079898600007666_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90011-3"},{"key":"S1079898600007666_ref047","first-page":"46","volume-title":"Proceedings of the 18th IEEE symposium on foundations of computer science","author":"Pnueli","year":"1977"},{"key":"S1079898600007666_ref031","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"S1079898600007666_ref001","unstructured":"van Benthem J. F. A. K. , Modal correspondence theory, Ph.D. thesis , University of Amsterdam, 1976."},{"key":"S1079898600007666_ref027","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E. , Otto M. , and Rosen E. , Undecidability results for two-variable logics, unpublished manuscript, 1996.","DOI":"10.1007\/BFb0023464"},{"key":"S1079898600007666_ref018","first-page":"137","article-title":"Alternation and the Ackermann case of the decision problem","volume":"27","author":"F\u00fcrer","year":"1981","journal-title":"L'Enseignment Mathematique"},{"key":"S1079898600007666_ref002","volume-title":"Modal logic and classical logic","author":"van Benthem","year":"1985"},{"key":"S1079898600007666_ref052","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449155"},{"key":"S1079898600007666_ref003","volume-title":"Report x-91-05","author":"van Benthem","year":"1991"},{"key":"S1079898600007666_ref057","volume-title":"Descriptive complexity and finite models","author":"Vardi","year":"1997"},{"key":"S1079898600007666_ref013","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"S1079898600007666_ref015","volume-title":"The decision problem: Solvable classes of quantificational formulas","author":"Dreben","year":"1979"},{"key":"S1079898600007666_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"S1079898600007666_ref044","first-page":"463","volume-title":"Machine intelligence 4","author":"McCarthy","year":"1969"},{"key":"S1079898600007666_ref028","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"S1079898600007666_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF01651329"},{"key":"S1079898600007666_ref038","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90021-7"},{"key":"S1079898600007666_ref056","first-page":"266","volume-title":"Proceedings of the 14th ACM symposium on principles of database systems","author":"Vardi","year":"1995"},{"key":"S1079898600007666_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"S1079898600007666_ref011","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192"},{"key":"S1079898600007666_ref012","doi-asserted-by":"publisher","DOI":"10.2307\/2269030"},{"key":"S1079898600007666_ref046","volume-title":"Bounded variable logics and counting\u2014a study in finite models","author":"Otto","year":"1995"},{"key":"S1079898600007666_ref019","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/3-540-13331-3_48","volume-title":"Logical machines: Decision problems and complexity","volume":"171","author":"F\u00fcrer","year":"1981"},{"key":"S1079898600007666_ref030","volume-title":"Report","author":"Henkin","year":"1967"},{"key":"S1079898600007666_ref036","doi-asserted-by":"publisher","DOI":"10.1007\/BF01452848"},{"key":"S1079898600007666_ref034","first-page":"334","volume-title":"Proceedings of the 6th IEEE symposium on structure in complexity theory","author":"Immerman","year":"1991"},{"key":"S1079898600007666_ref008","first-page":"325","volume-title":"Proceedings of the 2nd conference on theoretical aspects of reasoning about knowledge","author":"Burrows","year":"1988"},{"key":"S1079898600007666_ref022","first-page":"306","article-title":"Zum Entscheidungsproblem des logischen Funktionenkalk\u00fcls","volume":"40","author":"G\u00f6del","year":"1933","journal-title":"Monatshefte f\u00fcr Mathematik Phys."},{"key":"S1079898600007666_ref041","volume-title":"Unsolvable classes of quantificational formulas","author":"Lewis","year":"1979"},{"key":"S1079898600007666_ref048","first-page":"109","volume-title":"Proceedings of the 17th IEEE symposium on foundations of computer science","author":"Pratt","year":"1976"},{"key":"S1079898600007666_ref005","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1675978"},{"key":"S1079898600007666_ref020","first-page":"91","volume-title":"Aspects of philosophical logic","author":"Gabbay","year":"1971"},{"key":"S1079898600007666_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51498-8_21"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600007666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T21:22:24Z","timestamp":1557609744000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600007666\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,3]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1997,3]]}},"alternative-id":["S1079898600007666"],"URL":"https:\/\/doi.org\/10.2307\/421196","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,3]]}}}