<abstract xmlns="http://www.w3.org/1999/xhtml">The main purpose of formalization is to prove that two equations y<italic>a</italic>(<italic>z</italic>)= <italic>y</italic>, <italic>y</italic> = <italic>xz</italic> are Diophantine. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.In our previous work [6], we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities. In this formalization, we express these relations in terms of Diophantine set introduced in <xref ref-type="bibr" rid="j_forma-2018-0015_ref_007_w2aab3b7b7b1b6b1ab1ab7Aa">[7]</xref>. We prove that these relations are Diophantine and then we prove several second-order theorems that provide the ability to combine Diophantine relation using conjunctions and alternatives as well as to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation. Finally, we investigate the possibilities of our approach to prove that the two equations, being the main purpose of this formalization, are Diophantine.The formalization by means of Mizar system <xref ref-type="bibr" rid="j_forma-2018-0015_ref_003_w2aab3b7b7b1b6b1ab1ab3Aa">[3]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0015_ref_002_w2aab3b7b7b1b6b1ab1ab2Aa">[2]</xref> follows Z. Adamowicz, P. Zbierski <xref ref-type="bibr" rid="j_forma-2018-0015_ref_001_w2aab3b7b7b1b6b1ab1ab1Aa">[1]</xref> as well as M. Davis <xref ref-type="bibr" rid="j_forma-2018-0015_ref_004_w2aab3b7b7b1b6b1ab1ab4Aa">[4]</xref>.</abstract>

The main purpose of formalization is to prove that two equations ya(z)= y, y = xz are Diophantine. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.In our previous work [6], we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities. In this formalization, we express these relations in terms of Diophantine set introduced in [7]. We prove that these relations are Diophantine and then we prove several second-order theorems that provide the ability to combine Diophantine relation using conjunctions and alternatives as well as to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation. Finally, we investigate the possibilities of our approach to prove that the two equations, being the main purpose of this formalization, are Diophantine.The formalization by means of Mizar system [3], [2] follows Z. Adamowicz, P. Zbierski [1] as well as M. Davis [4].

Basic Diophantine Relations

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Basic Diophantine Relations"}

The main purpose of formalization is to prove that two equations ya(z)= y, y = xz are Diophantine. These equations are explored in the proof of Matiyasevich’s...

Basic Diophantine Relations

Publié en ligne: 24 déc. 2018

Pages: 175 - 181

Accepté: 29 juin 2018

DOI: https://doi.org/10.2478/forma-2018-0015

Mots clés
Hilbert’s 10th problem, Diophantine relations

© 2018 Marcin Acewicz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Basic Diophantine Relations

Publié en ligne: 24 déc. 2018

Pages: 175 - 181

Accepté: 29 juin 2018

DOI: https://doi.org/10.2478/forma-2018-0015

Mots clésHilbert’s 10th problem, Diophantine relations

© 2018 Marcin Acewicz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Mots clés
Hilbert’s 10th problem, Diophantine relations