{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T07:47:45Z","timestamp":1715240865944},"reference-count":26,"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":6585,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1996,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count.<\/jats:p><jats:p>To this end an isomorphism preserving (\u2018generic\u2019) model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved.<\/jats:p><jats:p>In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200017680_inline1\" \/>and the corresponding pebble games.<\/jats:p><jats:p>The main result, however, involves the concept of an<jats:italic>arithmetical invariant<\/jats:italic>. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200017680_inline2\" \/>with the following properties:<\/jats:p><jats:p>\u2022 The invariants themselves can be evaluated in polynomial time.<\/jats:p><jats:p>\u2022 A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.<\/jats:p><jats:p>\u2022 The invariant<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200017680_inline3\" \/><jats:sup><jats:italic>r<\/jats:italic><\/jats:sup>classifies all finite relational structures exactly up to equivalence with respect to the logic<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200017680_inline1\" \/><\/jats:p><jats:p>We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200017680_inline1\" \/>: It corresponds exactly to the polynomial time computable families (<jats:italic>\u03c6<\/jats:italic><jats:sub><jats:italic>n<\/jats:italic><\/jats:sub>)<jats:sub><jats:italic>n<\/jats:italic>\u2208<jats:italic>\u03c9<\/jats:italic><\/jats:sub>in these logics.<\/jats:p><jats:p>Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindstr\u00f6m quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindstr\u00f6m quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting.<\/jats:p>","DOI":"10.2307\/2275602","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:57:36Z","timestamp":1146956256000},"page":"147-176","source":"Crossref","is-referenced-by-count":24,"title":["The expressive power of fixed-point logic with counting"],"prefix":"10.1017","volume":"61","author":[{"given":"Martin","family":"Otto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200017680_ref007","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1084"},{"key":"S0022481200017680_ref024","first-page":"373","volume":"27","author":"Rescher","year":"1962","journal-title":"Plurality quantification"},{"key":"S0022481200017680_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80029-8"},{"key":"S0022481200017680_ref009","first-page":"231","volume-title":"Computer science logic, selected papers from CSL '92","author":"Gr\u00e4del","year":"1993"},{"key":"S0022481200017680_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56039-4_36"},{"key":"S0022481200017680_ref002","volume-title":"Proceedings of the 7th IEEE conference on structure in complexity theory","author":"Abiteboul","year":"1992"},{"key":"S0022481200017680_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0099486"},{"key":"S0022481200017680_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(91)90032-Z"},{"key":"S0022481200017680_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90055-2"},{"key":"S0022481200017680_ref015","first-page":"31","volume-title":"Colloqium on the foundations of mathematics, mathematical machines and their application","author":"H\u00e4rtig","year":"1965"},{"key":"S0022481200017680_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4478-3_5"},{"key":"S0022481200017680_ref010","volume-title":"Diplomarbeit","author":"Grohe","year":"1992"},{"key":"S0022481200017680_ref026","volume-title":"The complexity of Boolean functions","author":"Wegener","year":"1987"},{"key":"S0022481200017680_ref005","first-page":"209","volume-title":"Proceedings of the 23rd ACM symposium on theory of computing","author":"Abiteboul","year":"1991"},{"key":"S0022481200017680_ref011","first-page":"124","volume-title":"Proceedings of the international conference on database theory","author":"Grumbach","year":"1992"},{"key":"S0022481200017680_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305232"},{"key":"S0022481200017680_ref008","first-page":"25","volume-title":"Model-theoretic logics","author":"Ebbinghaus","year":"1985"},{"key":"S0022481200017680_ref012","first-page":"210","volume-title":"Proceedings of the 24th IEEE symposium on foundations of computer science","author":"Gurevich","year":"1983"},{"key":"S0022481200017680_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90011-3"},{"key":"S0022481200017680_ref018","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1109\/PSCT.1987.10319271","volume-title":"Proceedings of the 2nd conference on structure in complexity theory","author":"Immerman","year":"1987"},{"key":"S0022481200017680_ref019","first-page":"75","volume-title":"Computational complexity theory, proceedings of the AMS symposium in applied mathematics","volume":"38","author":"Immerman","year":"1989"},{"key":"S0022481200017680_ref021","first-page":"348","volume-title":"Proceedings of the 7th IEEE symposium on logic in computer science","author":"Kolaitis","year":"1992"},{"key":"S0022481200017680_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90021-7"},{"key":"S0022481200017680_ref023","volume-title":"Proceedings of the 9th IEEE symposium on logic in computer science","author":"Otto","year":"1994"},{"key":"S0022481200017680_ref025","first-page":"137","volume-title":"Proceedings of the 14th ACM symposium on theory of computing","author":"Vardi","year":"1982"},{"key":"S0022481200017680_ref003","first-page":"71","volume-title":"Proceedings of the 4th IEEE symposium on logic in computer science","author":"Abiteboul","year":"1989"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200017680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:28:31Z","timestamp":1707031711000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200017680\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["S0022481200017680"],"URL":"https:\/\/doi.org\/10.2307\/2275602","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}