Defining long words succinctly in FO and MSO

Lauri Hella; Miikka Vilander

doi:10.3233/COM-230450

Defining long words succinctly in FO and MSO

Lauri Hella^*
, Miikka Vilander

^*Tämän työn vastaava kirjoittaja

Tutkimustuotos: Artikkeli › Tieteellinen › vertaisarvioitu

33 Lataukset (Pure)

Abstrakti

We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. For the two-variable fragment of FO we obtain quadratic lower and upper bounds for the definability numbers of quantifier rank k fragments. In addition, we consider the Löwenheim-Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.

Alkuperäiskieli	Englanti
Sivut	377-398
Sivumäärä	22
Julkaisu	Computability
Vuosikerta	13
Numero	3-4
DOI - pysyväislinkit	https://doi.org/10.3233/COM-230450
Tila	Julkaistu - 28 marrask. 2024
OKM-julkaisutyyppi	A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Rahoitus

Miikka Vilander was supported by the Academy of Finland projects Explaining AI via Logic (XAILOG), grant number 345612 (Kuusisto) and Theory of computational logics, grant numbers 352419, 352420, 353027, 324435 and 328987. We would also like to thank an anonymous reviewer for an improvement on the results of Theorem as well as all of their other hard work.

Rahoittajat	Rahoittajan numero
Research Council of Finland	324435, 352419, 352420, 328987, 353027, 345612

Julkaisufoorumi-taso

Jufo-taso 1

!!ASJC Scopus subject areas

Theoretical Computer Science
Computer Science Applications
Computational Theory and Mathematics
Artificial Intelligence

Pääsy asiakirjaan

10.3233/COM-230450Lisenssi: CC BY

com_2024_13-3-4_com-13-3-4-com230450_com-13-com230450-1Final published version, 226 KBLisenssi: CC BY

https://urn.fi/URN:NBN:fi:tuni-202502192275Lisenssi: CC BY

Siteeraa tätä

@article{f31116eb4fe94abdae6d83241c61d223,

title = "Defining long words succinctly in FO and MSO",

abstract = "We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. For the two-variable fragment of FO we obtain quadratic lower and upper bounds for the definability numbers of quantifier rank k fragments. In addition, we consider the L{\"o}wenheim-Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.",

keywords = "Logic on words, monadic second-order logic, succinctness",

author = "Lauri Hella and Miikka Vilander",

note = "Publisher Copyright: {\textcopyright} 2024 - The authors. Published by IOS Press.",

year = "2024",

month = nov,

day = "28",

doi = "10.3233/COM-230450",

language = "English",

volume = "13",

pages = "377--398",

journal = "Computability",

issn = "2211-3568",

publisher = "Sage Publications",

number = "3-4",

}

TY - JOUR

T1 - Defining long words succinctly in FO and MSO

AU - Hella, Lauri

AU - Vilander, Miikka

PY - 2024/11/28

Y1 - 2024/11/28

N2 - We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. For the two-variable fragment of FO we obtain quadratic lower and upper bounds for the definability numbers of quantifier rank k fragments. In addition, we consider the Löwenheim-Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.

AB - We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. For the two-variable fragment of FO we obtain quadratic lower and upper bounds for the definability numbers of quantifier rank k fragments. In addition, we consider the Löwenheim-Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.

KW - Logic on words

KW - monadic second-order logic

KW - succinctness

U2 - 10.3233/COM-230450

DO - 10.3233/COM-230450

M3 - Article

AN - SCOPUS:85210909092

SN - 2211-3568

VL - 13

SP - 377

EP - 398

JO - Computability

JF - Computability

IS - 3-4

ER -

Defining long words succinctly in FO and MSO

Abstrakti

Rahoitus

Julkaisufoorumi-taso

!!ASJC Scopus subject areas

Pääsy asiakirjaan

Sormenjälki

Siteeraa tätä