<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

Published Online: Dec 24, 2018

Page range: 175 - 181

Accepted: Jun 29, 2018

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

Keywords
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

Published Online: Dec 24, 2018

Page range: 175 - 181

Accepted: Jun 29, 2018

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

KeywordsHilbert’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.

Keywords
Hilbert’s 10th problem, Diophantine relations