Decidability bounds for extensions of Presburger arithmetic

Blanchard, Eion

Permalink

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

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

Copyright and License Information

Copyright 2023 Eion Blanchard

Owning Collections