:: Formalization of the {MRDP } Theorem in the {M}izar System
:: by Karol P\kak
::
:: Received May 27, 2019
:: Copyright (c) 2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
FUNCT_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3, ZFMISC_1, CARD_1,
ORDINAL1, ARYTM_1, PRE_POLY, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1,
VECTSP_1, POLYNOM1, POLYNOM2, AFINSQ_1, COMPLEX1, SQUARE_1, NEWTON,
HILB10_2, INT_2, PARTFUN3, REWRITE2, REAL_1, VALUED_0, FINSEQ_2, CARD_3,
REALSET1, STRUCT_0, SGRAPH1, BINOP_2, PARTFUN1, INT_6, ORDERS_1,
FINSET_1, SUPINF_2, FUNCOP_1, WELLORD2, ALGSEQ_1, UPROOTS, MEMBERED,
RFINSEQ, JORDAN3, FUNCT_2, HILBASIS, FUNCT_4, HILB10_5;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, RELSET_1,
FUNCT_1, FINSET_1, XCMPLX_0, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, NAT_1,
ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VECTSP_1,
GROUP_1, GROUP_4, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1, XREAL_0, INT_1,
POLYNOM2, AFINSQ_1, AFINSQ_2, COMPLEX1, SQUARE_1, NEWTON, HILB10_2,
XXREAL_2, VALUED_0, FINSEQ_2, RVSUM_1, VALUED_1, BINOP_2, MEMBERED,
INT_2, REWRITE2, INT_6, WSIERP_1, FINSEQOP, UPROOTS, PARTFUN3, CARD_1,
NAT_D, HILBASIS, POLYNOM7, HILB10_4;
constructors NAT_D, RECDEF_1, BINOP_2, RELSET_1, GROUP_4, POLYNOM2, AFINSQ_2,
SQUARE_1, NEWTON, HILB10_2, XXREAL_2, WSIERP_1, INT_6, TRIANG_1,
FINSEQOP, FINSOP_1, UPROOTS, REWRITE2, ALGSTR_1, HILBASIS, POLYNOM7,
HILB10_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1,
VALUED_0, VALUED_1, RELSET_1, INT_1, PEPIN, STRUCT_0, VECTSP_1, PRE_POLY,
MEMBERED, POLYNOM2, AFINSQ_1, HILB10_2, XXREAL_2, XXREAL_0, FINSET_1,
XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON04,
MOEBIUS2, EUCLID_9, OSALG_1, REWRITE2, INT_6, FOMODEL0, FOMODEL2,
AFINSQ_2, FUNCOP_1, WSIERP_1, ALGSTR_1, ALGSTR_0, HILBASIS, POLYNOM7,
HILB10_3, FUNCT_2, HILB10_4;
requirements NUMERALS, SUBSET, ARITHM, REAL;
begin :: Preliminaries
reserve i,j,n,n1,n2,m,k,l,u for Nat,
i1,i2,i3,i4,i5,i6 for Element of n,
p,q for n-element XFinSequence of NAT,
a,b,c,d,e,f for Integer;
registration
let n be Nat;
cluster idseq n -> INT -valued;
let x be n-element natural-valued XFinSequence;
let p be INT -valued Polynomial of n,F_Real;
cluster eval(p,@x) -> integer;
end;
theorem :: HILB10_5:1
for p being INT -valued Polynomial of n, F_Real
for x,y being n-element XFinSequence of NAT st k<>0 &
for i st i in n holds k divides (x.i - y.i) holds
k divides (eval(p,@x) qua Integer) - (eval(p,@y) qua Integer);
registration
let f be INT -valued Function;
cluster - f -> INT -valued;
end;
scheme :: HILB10_5:sch 1
SCH1{P[object,object],f() -> XFinSequence-yielding XFinSequence}:
{f().i.j where i,j is Nat:P[i,j]} is finite;
theorem :: HILB10_5:2
m >= n > 0 implies
1+(m! * idseq n) is CR_Sequence;
theorem :: HILB10_5:3
for p being Prime
for f being FinSequence of NAT st
f is positive-yielding & p divides Product f
ex i st i in dom f & p divides f.i;
begin :: Selected operations on polynomials
definition
let n be set, p be Series of n, F_Real;
func |. p .| -> Series of n,F_Real means
:: HILB10_5:def 1
for b being bag of n holds it.b = |. p.b .|;
end;
theorem :: HILB10_5:4
for n being set, p being Series of n, F_Real holds
Support p = Support |. p .|;
registration
let n be Ordinal;
let p be Polynomial of n, F_Real;
cluster |. p .| -> finite-Support;
end;
registration
let n be set;
let S be non empty ZeroStr;
let p be finite-Support Series of n, S;
cluster Support p -> finite;
end;
definition
let n be Ordinal;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Polynomial of n, L;
func sum_of_coefficients p -> Element of L equals
:: HILB10_5:def 2
Sum (p * SgmX(BagOrder n,Support p));
end;
definition
let n be Ordinal;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Polynomial of n, L;
func degree p -> Nat means
:: HILB10_5:def 3
(ex s being bag of n st s in Support p &
it = degree s) &
for s1 being bag of n st s1 in Support p holds
degree s1 <= it
if p <> 0_(n,L) otherwise it = 0;
end;
theorem :: HILB10_5:5
for n being Ordinal, b being bag of n holds
degree b = Sum (b * SgmX(RelIncl n, support b));
theorem :: HILB10_5:6
for n being Ordinal,L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of n, L holds
degree p = 0 iff Support p c= {EmptyBag n};
theorem :: HILB10_5:7
for n being Ordinal,L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of n, L, b being bag of n st b in Support p holds
degree p >= degree b;
theorem :: HILB10_5:8
for n being Ordinal,p being Polynomial of n, F_Real st
|.p.| = 0_(n,F_Real) holds p = 0_(n,F_Real);
registration
let n be set;
reduce |. 0_(n,F_Real) .| to 0_(n,F_Real);
end;
theorem :: HILB10_5:9
for n being Ordinal,p being Polynomial of n, F_Real holds
degree p = degree |. p .|;
theorem :: HILB10_5:10
for n being Ordinal,b being bag of n,r being Real st r >= 1
for x being Function of n, the carrier of F_Real st
for i being object st i in dom x holds |. x.i .| <= r holds
|. eval(b,x).| <= r |^ (degree b);
theorem :: HILB10_5:11
for n being Ordinal,p being Polynomial of n, F_Real,
r being Real st r >= 1
for x being Function of n, the carrier of F_Real st
for i being object st i in dom x holds |. x.i .| <= r
holds
|. eval(p,x).| <= (sum_of_coefficients |.p.|) * (r|^ degree p);
registration
let n be Ordinal,p be INT -valued Polynomial of n, F_Real;
cluster |.p.| -> natural-valued;
end;
registration
let n be Ordinal;
cluster natural-valued for Polynomial of n, F_Real;
end;
registration
let O be Ordinal,p be natural-valued Polynomial of O, F_Real;
cluster sum_of_coefficients p -> natural;
end;
begin :: Selected subsets of zero based finite sequences of NAT
:: as diophantine sets
scheme :: HILB10_5:sch 2
SubsetDioph{n()->Nat, P[Nat,Nat,Nat,Nat],S() ->set}:
for i2,i3,i4 be Element of n() holds
{p where p is n()-element XFinSequence of NAT:
for i being Nat st i in S() holds P[p.i,p.i2,p.i3,p.i4]}
is diophantine Subset of n() -xtuples_of NAT
provided
for i1,i2,i3,i4 being Element of n() holds
{p where p is n()-element XFinSequence of NAT: P[p.i1,p.i2,p.i3,p.i4]}
is diophantine Subset of n() -xtuples_of NAT
and
S() c= Segm n();
theorem :: HILB10_5:12
for k,n1,n2,i,j,l,m,n,i1,i2,i3,i4 st n1+n2 <= n holds
{p: p.i1 >= k *
(((p.i2)^2+1)* (Product (1+((p/^n1)|n2) ))*(l*p.i3+m)) |^
(i*(p.i4)+j)}
is diophantine Subset of n -xtuples_of NAT;
theorem :: HILB10_5:13
for P being INT -valued Polynomial of k,F_Real, a being Integer,
perm being Permutation of n,i1 st k <= n
holds
{p: for q be k-element XFinSequence of NAT st q = (p*perm)|k holds
a * (p.i1) = eval(P,@q)}
is diophantine Subset of n -xtuples_of NAT;
theorem :: HILB10_5:14
for P being INT -valued Polynomial of k+1,F_Real,a being Integer,
n,i1,i2 st k+1 <= n & k in i2
holds
{p: for q being k+1-element XFinSequence of NAT st q = <%p.i2%>^(p|k) holds
a* p.i1 = eval(P,@q)}
is diophantine Subset of n -xtuples_of NAT;
theorem :: HILB10_5:15
for P being INT -valued Polynomial of k+1,F_Real,n,i1,i2 st
k+1 <= n & k in i1
holds
{p: for q be k+1-element XFinSequence of NAT st q = <%p.i1%>^(p|k) holds
eval(P,@q),0 are_congruent_mod p.i2}
is diophantine Subset of n -xtuples_of NAT;
begin :: Bounded quantifier theorem and its variant
theorem :: HILB10_5:16
for p being INT -valued Polynomial of 2+n+k,F_Real,
X being n-element XFinSequence of NAT,
x be Element of NAT holds
( for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0) iff
ex Y being k-element XFinSequence of NAT,
Z,e,K being Element of NAT st
K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X))*e)|^degree p &
(for i being Nat st i in k holds Y.i > e) &
e > x &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i being Nat st i in k holds
Product ((Y.i + 1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!)));
theorem :: HILB10_5:17
for p being INT -valued Polynomial of 2+n+k,F_Real,
X being n-element XFinSequence of NAT,
x being Element of NAT holds
( for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x)&
eval(p,@(<%z,x%>^X^y)) = 0)
iff
ex Y being k-element XFinSequence of NAT,
Z,K being Element of NAT st
K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X)))|^degree p &
(for i being Nat st i in k holds Y.i > (x+1)) &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i being Nat st i in k holds
Product ((Y.i + 1)+(-idseq (x+1))),
0 are_congruent_mod (1+(Z+1)*(K!)));
theorem :: HILB10_5:18
for p being INT -valued Polynomial of 2+n+k,F_Real holds
{X where X is n-element XFinSequence of NAT:
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0}
is diophantine Subset of n -xtuples_of NAT;
theorem :: HILB10_5:19
for p being INT -valued Polynomial of 2+n+k,F_Real holds
{X where X is n-element XFinSequence of NAT:
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
(for i being Nat st i in k holds y.i <= x) &
eval(p,@(<%z,x%>^X^y)) = 0}
is diophantine Subset of n -xtuples_of NAT;
::$N Davis Normal Form
definition
let n be Nat;
let A be Subset of n -xtuples_of NAT;
attr A is recursively_enumerable means
:: HILB10_5:def 4
ex m being Nat, P being INT -valued Polynomial of 2+n+m,F_Real st
for X being n -element XFinSequence of NAT holds
X in A
iff
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i being object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0;
end;
theorem :: HILB10_5:20
for n being Nat
for A being Subset of n -xtuples_of NAT holds
A is diophantine implies A is recursively_enumerable;
begin :: MRDP Theorem
::$N Yuri Matiyasevich, Julia Robinson, Martin Davis, Hilary Putnam Theorem
theorem :: HILB10_5:21
for n being Nat
for A being Subset of n -xtuples_of NAT holds
A is recursively_enumerable implies A is diophantine;