theoremnovelinferred_depunresolved_ref

Hilbert's tenth problem over Q is undecidable

Solvability of polynomials over Q is undecidable
the headline result
Theorem·thm:main·§1 Introduction

Statement (paper)

There is no algorithm which, given a polynomial f∈Z[X1,…,Xn]f\in\Z[X_1,\ldots,X_n], with nn part of the input, decides whether ff has a zero in Qn\Q^n.

In plain English

No algorithm can take a polynomial f∈Z[X1,…,Xn]f\in\Z[X_1,\ldots,X_n], with nn part of the input, and decide whether ff has a zero in Qn\Q^n.

Why it's here

This is the paper's main result. It is obtained by reducing integer solvability (Hilbert's tenth problem over Z\Z) to rational solvability. The two dependencies supply the reduction: the recursive theory T\mathcal T has the standard integers as a model, and if all finite rational tests for ff are solvable then ff has an integer zero. A rational decision procedure would therefore decide integer solvability, which is impossible.
Classified novel:
Undecidability of Hilbert's tenth problem over Q has been a long-standing open problem; Matiyasevich's theorem (1970) covers only Z, and no prior reduction from integer to rational solvability was known. The paper's reduction through finite rational tests and the recursive theory T is its central new contribution.

Uses

propFinite test success gives integer zerolemIntegers form a model of the theory

Used by

corDegree 0' for rational solvability and quartic formsclaimOracle reduces integer to rational solvability

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
thm:main
Line
sections/01-introduction.tex:7
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The proof says "Their answers are sound" (02-reduction.tex:884). Soundness of a failed test rests on the integer model of Lemma red:standard-model, as stated at lines 540-543: "an integer zero extends the model of Lemma ".
  • warn
    unresolved_ref
    Final contradiction relies on the external DPRM theorem.