Diophantine sets and Hilbert's tenth problem

DefinitionDiophantine sets#✓fully proved

Let \(\varphi : A \to R\) be a ring homomorphism of commutative rings and let \(k \in \mathbb{N}\). Polynomials with coefficients in \(A\) are evaluated at points with coordinates in \(R\) by first mapping their coefficients into \(R\) by \(\varphi\). A subset \(S \subseteq R^k\) is Diophantine over \(R\) with coefficients from \(A\) through \(\varphi\) when there are \(n \in \mathbb{N}\) and a finite set \(P\) of polynomials with coefficients in \(A\) in the variables \(x_1, \dots, x_k, y_1, \dots, y_n\) such that for every \(x \in R^k\), \(x \in S\) if and only if there is \(y \in R^n\) with \(p(x, y) = 0\) for all \(p \in P\).

def IsDiophantine (φ : A →+* R) {k : ℕ} (S : Set (Fin k → R)) : Prop :=
  ∃ (n : ℕ) (P : Finset (MvPolynomial (Fin k ⊕ Fin n) A)), ∀ x : Fin k → R,
    x ∈ S ↔ ∃ y : Fin n → R, ∀ p ∈ P, eval₂ φ (Sum.elim x y) p = 0

Used by 3

Used byThe empty set is Diophantine · Diophantine subsets of a ring · The whole space is Diophantine

DefinitionDiophantine subsets of a ring#✓fully proved

Let \(\varphi : A \to R\) be a ring homomorphism of commutative rings. A subset \(S \subseteq R\) is Diophantine over \(R\) with coefficients from \(A\) through \(\varphi\) when the set \(\{(s) : s \in S\} \subseteq R^1\) of one-coordinate points with coordinate in \(S\) is a Diophantine subset of \(R^1\) over \(R\) with coefficients from \(A\) through \(\varphi\).

def IsDiophantineSet (φ : A →+* R) (S : Set R) : Prop :=
  IsDiophantine φ {x : Fin 1 → R | x 0 ∈ S}

Uses 1

Statement usesDiophantine sets

TheoremThe whole space is Diophantine#✓fully proved

Let \(\varphi : A \to R\) be a ring homomorphism of commutative rings. For every \(k \in \mathbb{N}\), the whole space \(R^k\) is Diophantine over \(R\) with coefficients from \(A\) through \(\varphi\).

It is cut out by the empty set of polynomials, with no auxiliary variables.

theorem isDiophantine_univ (φ : A →+* R) (k : ℕ) :
    IsDiophantine φ (Set.univ : Set (Fin k → R))

Uses 1

Statement usesDiophantine sets

TheoremThe empty set is Diophantine#✓fully proved

Let \(\varphi : A \to R\) be a ring homomorphism of commutative rings, with \(R\) nontrivial. For every \(k \in \mathbb{N}\), the empty subset of \(R^k\) is Diophantine over \(R\) with coefficients from \(A\) through \(\varphi\).

It is cut out by the constant polynomial \(1\).

theorem isDiophantine_empty [Nontrivial R] (φ : A →+* R) (k : ℕ) :
    IsDiophantine φ (∅ : Set (Fin k → R))

Uses 1

Statement usesDiophantine sets

TheoremDavis–Putnam–Robinson–Matiyasevich theorem#✓fully proved

A set \(S\) of natural numbers is recursively enumerable if and only if it is Diophantine, that is, there is a polynomial \(p\) with integer coefficients such that \(n \in S\) exactly when \(p(n, t_1, \dots, t_k) = 0\) for some natural numbers \(t_1, \dots, t_k\).

public theorem dprm_theorem
    (S : Set ℕ) : REPred (fun n => n ∈ S) ↔ Dioph {v : Unit → ℕ | v () ∈ S}

Sources

• M. Davis, H. Putnam, J. Robinson, The decision problem for exponential Diophantine equations, Ann. of Math. 74 (1961); Y. Matiyasevich, Enumerable sets are Diophantine, Dokl. Akad. Nauk SSSR 191 (1970) 279–282; textbook in Matiyasevich, Hilbert's Tenth Problem

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.