Decidability bounds for extensions of Presburger arithmetic

This thesis considers undecidable logical theories extending or closely related to Presburger arithmetic, the decidable first-order theory of the natural numbers with order and addition. Through the primary lens of quantifier complexity rather than computational complexity, we develop explicit bounds for the threshold between decidable and undecidable fragments of such theories. In Chapter 2, we consider a generalized setting with the fragment of the first-order theory of a structure over the ordered real numbers with quantification restricted to a fixed subset. When the structure defines functions with sufficiently wild properties, we demonstrate how to encode the weak monadic second-order theory of the grid. With this, we simulate a Turing machine and thus encode the halting problem, which is undecidable, as a first-order sentence in the language at hand. This yields an upper bound for decidable fragments of such theories in terms of the quantifier complexity for defining a few basic tools. In each of Chapter 3, Chapter 4, and Chapter 5, we consider a particular theory and instantiate the main theorem from Chapter 2 to conclude that the set of sentences with four alternating quantifier blocks of a given minimum length is undecidable. In Chapter 3, we consider sine-Presburger arithmetic (sin-PA), which is the fragment of the first-order theory of (R, <, 0, 1, +, sin, N) in which quantification is restricted to N. We provide a decision procedure for the existential sentences in this theory that is conditioned by a positive answer to Schanuel’s conjecture, an open problem in number theory. In Chapter 4, we consider μ_{2,3}-linear real arithmetic (μ_{2,3}-LRA), which is the fragment of the first-order theory of (R, <, 0, 1, +, μ_{2,3}, 2^N) in which quantification is restricted to 2^N and μ_{2,3} : 2^N → [1, 3) is the function that divides a power of 2 by its preceding power of 3. We provide a decision procedure for the existential sentences in this theory that is conditioned by a positive answer to an open conjecture that the finitely many nondegenerate solutions to any linear equation over the multiplicative group B_{2,3} := 2^Z 3^Z are computable; this is deemed the effective Mann property of B_{2,3}. In Chapter 5, we consider A_{2,3}-real arithmetic (A_{2,3}-RA), which is the fragment of the first-order theory of (R, <, 0, 1, +, ·, A_{2,3}) in which quantification is restricted to A_{2,3} := 2^N ∪ 3^N. While we do not provide a full decision procedure for the existential sentences in this theory, we do conjecture its existence, again under assumption of the effective Mann property of B_{2,3}. As partial progress toward a positive answer to this conjecture, we reduce the decision problem for existential sentences in this theory to the decision problem for open existential sentences in the same signature with quantification restricted to 2^N and 3^N.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Mathematics

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2023

Author dc:creator

• Blanchard, Eion

Contributors dc:contributor

• Hieronymi, Philipp
• van den Dries, Lou
• Parthasarathy, Madhusudan
• Kishida, Kohei

• Mathematical Logic
• Model Theory
• Theoretical Computer Science
• Decidability
• Undecidability
• Presburger Arithmetic

Statement dc:rights

• Copyright 2023 Eion Blanchard

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/121510

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F121510