<abstract xmlns="http://www.w3.org/1999/xhtml">This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form <italic>x</italic>2<italic>−</italic> (<italic>a</italic>2 − 1)<italic>y</italic>2 = 1 [8] and its solutions considered as two sequences <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2019-0020_eq_001.png"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><msubsup><mrow><mrow><mrow><mo>{</mo><mrow><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub><mo>(</mo><mi>a</mi><mo>)</mo></mrow><mo>}</mo></mrow></mrow></mrow><mrow><mi>i</mi><mo>=</mo><mn>0</mn></mrow><mo>∞</mo></msubsup><mo>,</mo><msubsup><mrow><mrow><mrow><mo>{</mo><mrow><msub><mrow><mi>y</mi></mrow><mi>i</mi></msub><mo>(</mo><mi>a</mi><mo>)</mo></mrow><mo>}</mo></mrow></mrow></mrow><mrow><mi>i</mi><mo>=</mo><mn>0</mn></mrow><mo>∞</mo></msubsup></mrow></math><tex-math>$\left\{ {{x_i}(a)} \right\}_{i = 0}^\infty ,\left\{ {{y_i}(a)} \right\}_{i = 0}^\infty$</tex-math></alternatives></inline-formula>. We showed in [1] that the <italic>n</italic>-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation <italic>x</italic> = <italic>y</italic>i(<italic>a</italic>) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function <italic>y</italic> = <italic>x</italic>z is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9].In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that <italic>every recursively enumerable set is Diophantine,</italic> where recursively enumerable sets have been defined by the Martin Davis normal form.The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].</abstract>

This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form x2− (a2 − 1)y2 = 1 [8] and its solutions considered as two sequences {xi(a)}i=0∞,{yi(a)}i=0∞$\left\{ {{x_i}(a)} \right\}_{i = 0}^\infty ,\left\{ {{y_i}(a)} \right\}_{i = 0}^\infty$. We showed in [1] that the n-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation x = yi(a) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function y = xz is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9].In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that every recursively enumerable set is Diophantine, where recursively enumerable sets have been defined by the Martin Davis normal form.The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].

Formalization of the MRDP Theorem in the Mizar System

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Formalization of the MRDP Theorem in the Mizar System"}

This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.In our approach, we work with the Pell’s Equation...

Formalization of the MRDP Theorem in the Mizar System

Publicado en línea: 20 jul 2019

Páginas: 209 - 221

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0020

Palabras clave
Hilbert’s 10th problem, Diophantine relations

© 2019 Karol Pąk, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Formalization of the MRDP Theorem in the Mizar System

Publicado en línea: 20 jul 2019

Páginas: 209 - 221

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0020

Palabras claveHilbert’s 10th problem, Diophantine relations

© 2019 Karol Pąk, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Palabras clave
Hilbert’s 10th problem, Diophantine relations