In this paper we complete Büchi's proof that there is no decision algorithm for the solubility in integers of arbitrary systems of diagonal quadratic form equations, by proving the assertion that whenever $x_1^2, \cdots, x_5^2$ are five squares such that the second differences satisfy \[x_{k+2}^2 - 2 x_{k+1}^2 + x_k^2 = 2\] for $k = 1,2,3$, then they must be consecutive. This answers a question of J.~Richard~Büchi.

Expansions of the monadic second-order (MSO) theory of the structure ⟨ℕ;<⟩ have been a fertile and active area of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ⟨ℕ;<,P⟩, where P ranges over a large class of unary "dynamical" predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.

We prove that for any integers α, β > 1, the existential fragment of the first-order theory of the structure ⟨ℤ; 0,1,<, +,αℕ,ßℕ⟩ is decidable (where αℕ is the set of positive integer powers of α, and likewise for βℕ). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of ⟨ℕ; 0,1,<, +,x ↦ αx,x ↦ βχ⟩ for any multiplicatively independent α, β > 1 would lead to mathematical breakthroughs regarding base-α and base-β expansions of certain transcendental numbers. Finally, modifying the original proof of Hieronymi and Schulz we show that for any multiplicatively independent α, β > 1, it is undecidable whether a given formula with at most 3 alternating blocks of quantifiers holds in ⟨ℕ;0,1,<, +,αℕ,ßℕ⟩.

For which unary predicates P 1 , … , P m is the MSO theory of the structure 〈 N ; < , P 1 , … , P m 〉 decidable? We survey the state of the art, leading us to investigate combinatorial properties of almost-periodic, morphic, and toric words. In doing so, we show that if each P i can be generated by a toric dynamical system of a certain kind, then the attendant MSO theory is decidable. We give various applications of toric words, including the recent result of [1] that the MSO theory of 〈 N ; < , { 2 n : n ∈ N } , { 3 n : n ∈ N } 〉 is decidable.

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:

The Positivity Problem for linear recurrence sequences over a ring R of real algebraic numbers is to determine, given an LRS ${\left( {{u_n}} \right)_{n \in \mathbb{N}}}$ over R, whether un≥ 0 for all n. It is known to be Turing-equivalent to the following reachability problem: given a linear dynamical system (M, s) Rd×d×Rdand a halfspace H ⊆ ℝd, determine whether the orbit ${\left( {{M^n}s} \right)_{n \in \mathbb{N}}}$ ever enters H. The more general model-checking problem for LDS is to determine, given (M, s) and an ω-regular property φ over semialgebraic predicates T1,…, Tℓ⊆ ℝd, whether the orbit of (M, s) satisfies φ.In this paper, we establish the following1)The Positivity Problem for LRS over real algebraic numbers reduces to the Positivity Problem for LRS over the integers; and2)The model-checking problem for LDS with diagonalisable M is decidable subject to a Positivity oracle for simple LRS over the integers.In other words, the full semialgebraic model-checking problem for diagonalisable linear dynamical systems is no harder than the Positivity Problem for simple integer linear recurrence sequences. This is in sharp contrast with the situation for arbitrary (not necessarily diagonalisable) LDS and arbitrary (not necessarily simple) integer LRS, for which no such correspondence is expected to hold.

It is a longstanding open problem whether there is an algorithm to decide the Skolem Problem for linear recurrence sequences (LRS) over the integers, namely whether a given such sequence has a zero term (i.e., whether un = 0 for some n). A major breakthrough in the early 1980s established decidability for LRS of order 4 or less, i.e., for LRS in which every new term depends linearly on the previous four (or fewer) terms. The Skolem Problem for LRS of order 5 or more, in particular, remains a major open challenge to this day.

The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the Skolem Problem remains open. The main contribution of this paper is an algorithm to solve the Skolem Problem for simple linear recurrence sequences (those with simple characteristic roots). Whenever the algorithm terminates, it produces a stand-alone certificate that its output is correct - a set of zeros together with a collection of witnesses that no further zeros exist. We give a proof that the algorithm always terminates assuming two classical number-theoretic conjectures: the Skolem Conjecture (also known as the Exponential Local-Global Principle) and the p-adic Schanuel Conjecture. Preliminary experiments with an implementation of this algorithm within the tool Skolem point to the practical applicability of this method.