On the decidability of monadic second-order logic with arithmetic predicates
We investigate the decidability of the monadic second-order (MSO) theory of the structure ❬N; <, P1, … , Pk❭, for various unary predicates P1, …, Pk ⊆ N. We focus in particular on ‘arithmetic’ predicates arising in the study of linear recurrence sequences, such as fixed-base powers Powk = {kn : n...
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
2024
|
| _version_ | 1811140298051420160 |
|---|---|
| author | Berthé, V Karimov, T Nieuwveld, J Ouaknine, J Vahanwala, M Worrell, J |
| author_facet | Berthé, V Karimov, T Nieuwveld, J Ouaknine, J Vahanwala, M Worrell, J |
| author_sort | Berthé, V |
| collection | OXFORD |
| description | We investigate the decidability of the monadic second-order (MSO) theory of the structure ❬N; <, P1, … , Pk❭, for various unary predicates P1, …, Pk ⊆ N. We focus in particular on ‘arithmetic’ predicates arising in the study of linear recurrence sequences, such as fixed-base powers Powk = {kn : n ∈ N}, k-th powers Nk = {nk : n ∈ N}, and the set of terms of the Fibonacci sequence Fib = {0, 1, 2, 3, 5, 8, 13, …} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:
<ul><li>The MSO theory of ❬N; <, Pow2, Fib❭ is decidable; </li>
<li>The MSO theory of ❬N; <, Pow2, Pow3, Pow6❭ is decidable; </li>
<li>The MSO theory of ❬N; <, Pow2, Pow3, Pow5❭ is decidable assuming Schanuel's conjecture; </li>
<li>The MSO theory of ❬N; <, Pow4, N2❭ is decidable; </li>
<li>The MSO theory of ❬N; <, Pow2, N2❭ is Turing-equivalent to the MSO theory of ❬N; <, S❭, where S is the predicate corresponding to the binary expansion of √2. (As the binary expansion of √2 is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.) </li></ul>
These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory. |
| first_indexed | 2024-09-25T04:19:45Z |
| format | Conference item |
| id | oxford-uuid:fbfe077f-8523-4f78-b06f-279b00c844c4 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:19:45Z |
| publishDate | 2024 |
| record_format | dspace |
| spelling | oxford-uuid:fbfe077f-8523-4f78-b06f-279b00c844c42024-08-01T12:53:26ZOn the decidability of monadic second-order logic with arithmetic predicatesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fbfe077f-8523-4f78-b06f-279b00c844c4EnglishSymplectic Elements2024Berthé, VKarimov, TNieuwveld, JOuaknine, JVahanwala, MWorrell, JWe investigate the decidability of the monadic second-order (MSO) theory of the structure ❬N; <, P1, … , Pk❭, for various unary predicates P1, …, Pk ⊆ N. We focus in particular on ‘arithmetic’ predicates arising in the study of linear recurrence sequences, such as fixed-base powers Powk = {kn : n ∈ N}, k-th powers Nk = {nk : n ∈ N}, and the set of terms of the Fibonacci sequence Fib = {0, 1, 2, 3, 5, 8, 13, …} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following: <ul><li>The MSO theory of ❬N; <, Pow2, Fib❭ is decidable; </li> <li>The MSO theory of ❬N; <, Pow2, Pow3, Pow6❭ is decidable; </li> <li>The MSO theory of ❬N; <, Pow2, Pow3, Pow5❭ is decidable assuming Schanuel's conjecture; </li> <li>The MSO theory of ❬N; <, Pow4, N2❭ is decidable; </li> <li>The MSO theory of ❬N; <, Pow2, N2❭ is Turing-equivalent to the MSO theory of ❬N; <, S❭, where S is the predicate corresponding to the binary expansion of √2. (As the binary expansion of √2 is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.) </li></ul> These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory. |
| spellingShingle | Berthé, V Karimov, T Nieuwveld, J Ouaknine, J Vahanwala, M Worrell, J On the decidability of monadic second-order logic with arithmetic predicates |
| title | On the decidability of monadic second-order logic with arithmetic predicates |
| title_full | On the decidability of monadic second-order logic with arithmetic predicates |
| title_fullStr | On the decidability of monadic second-order logic with arithmetic predicates |
| title_full_unstemmed | On the decidability of monadic second-order logic with arithmetic predicates |
| title_short | On the decidability of monadic second-order logic with arithmetic predicates |
| title_sort | on the decidability of monadic second order logic with arithmetic predicates |
| work_keys_str_mv | AT berthev onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates AT karimovt onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates AT nieuwveldj onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates AT ouakninej onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates AT vahanwalam onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates AT worrellj onthedecidabilityofmonadicsecondorderlogicwitharithmeticpredicates |