925: Polynomials and PA/5

[Harvey Friedman]

In 924: Polynomials and PA/4,
https://cs.nyu.edu/pipermail/fom/2022-January/023106.html we stated
the following:

THEOREM 1. Let P_1,...,P_r:Z^n into Z^m be (dominating) integral
polynomials. There exists x_1 <* ... <* x_s from Z^m such that each
#(Pi,x_j) <= #(Pi,x_j+1).

This was stated wrong. Here is what I meant to say.

THEOREM 1. Let P_1,...,P_r:Z^n into Z^m be (dominating) integral
polynomials. There exists 0 < x_1 < ... < x_m+1 from Z^m such that each
#(P_i,x_1,...,x_m) <= #(P_i,x_2,...,x_m+1).

Here #(P,x_1,...,x_m) is the cardinality of the inverse image of
(x_1,...,x_m) under P.

Dominating means the sup norm of any argument is at most the sup norm
of the its value.

THEOREM 2. Theorem 1 with "dominating" is provably equivalent to
1-Con(PA) over EFA. This is the case even for r = 2.

THEOREM 3. Theorem 1 without "dominating" is provable in EFA +
2-Con(PA). Theorem 1 with r = 1 is provable in PA.

THEOREM 4. For each fixed m, Theorem 1 is provable in PA. This is not
the case for any finite fragment of PA even if we set r = 2.

There is a simple templating that is rather attractive.

TEMPLATE. Fix u in Z^2m.  Let P_1,...,P_r:Z^n into Z^m be (dominating) integral
polynomials. There exists (x,y) order equivaelnt to u such that each
#(P_i,x) <= #(P_i,y).

We should get effective comparability and well orderedness under
provable implications for, separately, the dominating case and the
general case without dominating. Also comparability under logical
strengths and interpretability, also effectively, and well ordered.
Also seems like these should be order type omega.

##########################################

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 925th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM
912: Base Theory Proposals for Third Order RM/5  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1  12/11/21  10:15PM
919: Proof Theory of Arithmetic/2  12/11/21  10:17PM
920: Polynomials and PA  1/7/22  4:35PM
921: Polynomials and PA/2  1/9/22  6:57 PM
922: WQO Games  1/10/22 5:32AM
923: Polynomials and PA/3  1/11/22  10:30 PM
924: Polynomials and PA/4  1/13/22  2:02 AM

Harvey Friedman