University of Illinois Urbana-Champaign

Decidability bounds for extensions of Presburger arithmetic

Blanchard, Eion

Content Files
BLANCHARD-DISSERTATION-2023.pdf

Permalink

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

Description

Title
Decidability bounds for extensions of Presburger arithmetic
Author(s)
Blanchard, Eion
Issue Date
2023-07-14
Director of Research (if dissertation) or Advisor (if thesis)
Hieronymi, Philipp
Doctoral Committee Chair(s)
van den Dries, Lou
Committee Member(s)
  • Parthasarathy, Madhusudan
  • Kishida, Kohei
Department of Study
Mathematics
Discipline
Mathematics
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
  • mathematical logic
  • model theory
  • theoretical computer science
  • decidability
  • undecidability
  • Presburger arithmetic
Abstract
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.
Graduation Semester
2023-08
Type of Resource
Thesis
Handle URL
https://hdl.handle.net/2142/121510
Copyright and License Information
Copyright 2023 Eion Blanchard

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois