{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:25Z","timestamp":1767927985370,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are strongly finitely witnessable and smooth are called <jats:italic>strongly polite<\/jats:italic> and can be effectively combined with other theories. Toledo, Zohar, and Barrett conjectured that stably infinite and strongly finitely witnessable theories are smooth and therefore strongly polite. They called counterexamples to this conjecture <jats:italic>unicorn theories<\/jats:italic>, as their existence seemed unlikely. We prove that, indeed, unicorns do not exist. We also prove versions of the L\u00f6wenheim\u2013Skolem theorem and the \u0141o\u015b\u2013Vaught test for many-sorted logic.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_34","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"658-675","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Nonexistence of\u00a0Unicorns and\u00a0Many-Sorted L\u00f6wenheim\u2013Skolem Theorems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5489-1733","authenticated-orcid":false,"given":"Benjamin","family":"Przybocki","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6539-398X","authenticated-orcid":false,"given":"Guilherme","family":"Toledo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"34_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer, Munich (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"34_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017).http:\/\/smt-lib.org"},{"key":"34_CR3","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, New York (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11, http:\/\/theory.stanford.edu\/~barrett\/pubs\/BT18.pdf","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Casal, F., Rasga, J.a.: Many-sorted equivalence of shiny and strongly polite theories. J. Automat. Reason. 60(2), 221\u2013236 (2018)","DOI":"10.1007\/s10817-017-9411-y"},{"key":"34_CR5","doi-asserted-by":"publisher","first-page":"50","DOI":"10.4064\/fm-43-1-50-68","volume":"43","author":"A Ehrenfeucht","year":"1956","unstructured":"Ehrenfeucht, A., Mostowski, A.: Models of axiomatic theories admitting automorphisms. Fund. Math. 43, 50\u201368 (1956)","journal-title":"Fund. Math."},{"key":"34_CR6","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)"},{"key":"34_CR7","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-04222-5_16","volume-title":"Frontiers of Combining Systems","author":"P Fontaine","year":"2009","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems, pp. 263\u2013278. Springer, Berlin Heidelberg, Berlin, Heidelberg (2009)"},{"key":"34_CR8","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. Tech. Rep. TR2010-922, Depatrment of Computer Science, New York University (Jan 2010). http:\/\/www.cs.stanford.edu\/~barrett\/pubs\/JB10-TR.pdf"},{"key":"34_CR9","doi-asserted-by":"publisher","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 602\u2013617. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_47","DOI":"10.1007\/978-3-540-71209-1_47"},{"key":"34_CR10","doi-asserted-by":"publisher","unstructured":"Kruskal, J.B.: The theory of well-quasi-ordering: a frequently discovered concept. J. Comb. Theory Ser. A 13, 297\u2013305 (1972). https:\/\/doi.org\/10.1016\/0097-3165(72)90063-5","DOI":"10.1016\/0097-3165(72)90063-5"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"\u0141\u00a0o\u015b, J.: On the categoricity in power of elementary deductive systems and some related problems. Colloquium Mathematicum 3, 58\u201362 (1954)","DOI":"10.4064\/cm-3-1-58-62"},{"key":"34_CR12","doi-asserted-by":"publisher","unstructured":"Marker, D.: Model theory: an introduction, Graduate Texts in Mathematics, vol. 217. Springer-Verlag, New York (2002). https:\/\/doi.org\/10.1007\/b98860","DOI":"10.1007\/b98860"},{"key":"34_CR13","doi-asserted-by":"publisher","unstructured":"Monk, J.D.: Mathematical Logic. Springer, New York (1976).https:\/\/doi.org\/10.1007\/978-1-4684-9452-5","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"34_CR14","volume-title":"Many-sorted Logic and its Applications","author":"M Monzano","year":"1993","unstructured":"Monzano, M.: Introduction to many-sorted logic. In: Meinke, K., Tucker, J.V. (eds.) Many-sorted Logic and its Applications. Wiley professional computing, Wiley, New York (1993)"},{"key":"34_CR15","doi-asserted-by":"publisher","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (oct 1979).https:\/\/doi.org\/10.1145\/357073.357079","DOI":"10.1145\/357073.357079"},{"key":"34_CR16","unstructured":"Przybocki, B., Toledo, G., Zohar, Y., Barrett, C.: The nonexistence of unicorns and many-sorted L\u00f6wenheim\u2013Skolem theorems (2024). https:\/\/arxiv.org\/abs\/2406.18912"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. (2) 30(4), 264\u2013286 (1929)","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"34_CR18","doi-asserted-by":"publisher","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) 5th International Workshop on Frontiers of Combining Systems - FroCoS\u201905. Lecture Notes in Artificial Intelligence, vol.\u00a03717, pp. 48\u201364. Springer, Vienna\/Austria (Sep 2005https:\/\/doi.org\/10.1007\/11559306, https:\/\/hal.inria.fr\/inria-00000570","DOI":"10.1007\/11559306"},{"key":"34_CR19","doi-asserted-by":"publisher","unstructured":"Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.: Polite combination of algebraic datatypes. J. Autom. Reasoning 66(3), 331\u2013355 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09625-3","DOI":"10.1007\/s10817-022-09625-3"},{"key":"34_CR20","doi-asserted-by":"publisher","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. Tech. rep., Berlin, Heidelberg (2004).https:\/\/doi.org\/10.1007\/978-3-540-30227-8_53","DOI":"10.1007\/978-3-540-30227-8_53"},{"key":"34_CR21","doi-asserted-by":"publisher","unstructured":"de\u00a0Toledo, G.V., Zohar, Y., Barrett, C.W.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. In: CADE, Lecture Notes in Computer Science, vol. 14132, pp. 522\u2013541. Springer, Rome (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_30","DOI":"10.1007\/978-3-031-38499-8_30"},{"key":"34_CR22","doi-asserted-by":"publisher","unstructured":"de Toledo, G.V., Zohar, Y., Barrett, C.W.: Combining finite combination properties: finite models and busy beavers. In: FroCoS, Lecture Notes in Computer Science, vol. 14279, pp. 159\u2013175. Springer, Prague (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_9","DOI":"10.1007\/978-3-031-43369-6_9"},{"key":"34_CR23","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1016\/S1385-7258(54)50058-2","volume":"57","author":"RL Vaught","year":"1954","unstructured":"Vaught, R.L.: Applications of the L\u00f6wenheim-Skolem-Tarski theorem to problems of completeness and decidability. Nederl. Akad. Wetensch. Proc. 57, 467\u2013472 (1954)","journal-title":"Nederl. Akad. Wetensch. Proc."},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Wang, H.: Logic of many-sorted theories. J. Symbolic Logic 17(2), 105\u2013116 (1952). http:\/\/www.jstor.org\/stable\/2266241","DOI":"10.2307\/2266241"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:08:41Z","timestamp":1725934121000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}