H10UC

Uniform Diophantine constraint solvability

Preliminaries

The definitions below are mechanized in Problems/H10UC.v.

A constraint has the shape 1 + x + y ⋅ y ≐ z, where x, y, z ∈ 𝕍 range over variables. Constraints are mechanized as nat * nat * nat.

A valuation φ : 𝕍 → ℕ satisfies 1 + x + y ⋅ y ≐ z if 1 + φ (x) + φ (y) * φ (y) = φ (z), mechanized as h10uc_sem.

Problem instance (mechanized as H10UC_PROBLEM)

An instance of uniform Diophantine constraint solvability is a list of constraints.

Decision problem (mechanized as H10UC_SAT)

Given a list L of uniform Diophantine constraints, is there a valuation that satisfies each constraint in L?

Reduction

Undecidability of Uniform Diophantine constraint solvability is obtained by reduction from elementary Diophantine constraint solvability (H10C_SAT in Problems/H10C.v). The reduction is mechanized in Reductions/H10C_to_H10UC.v as

Theorem H10C_SAT_to_H10UC_SAT : H10C_SAT ⪯ H10UC_SAT.

and

Theorem H10UC_undec : Halt ⪯ H10UC_SAT.

Key ideas

Encode 0 and 1

For a, b, c ∈ ℕ such that

1 + a + a * a = b
1 + a + b * b = c
1 + b + a * a = c

we necessarily have a = 0 and b = 1.

Encode successor

For a, b ∈ ℕ such that 1 + b + 0 * 0 = a we necessarily have a = 1 + b.

Encode square

For a, b ∈ ℕ such that 1 + 0 + b * b = 1 + a we necessarily have a = b * b.

Encode double

For a, b ∈ ℕ such that 1 + a + b * b = (1 + b) * (1 + b) we necessarily have a = b + b.

Encode sum

For a, b, c ∈ ℕ such that 1 + (b + b) + (1 + c) * (1 + c) = 1 + (1 + (a + a)) + c * c we necessarily have a = b + c.

Encode product

For a, b, c ∈ ℕ such that 1 + (1 + (a + a) + b * b) + c * c = 1 + 1 + (b + c) * (b + c) we necessarily have a = b * c.