923: Polynomials and PA/3

[Harvey Friedman]

We have decided against the surjectivity conditions used in posting
921. So we are moving back to something more like posting 920.

920 has some typos and misstatements. I won't even bother to correct
them because what I write here obsoletes 920 and 921.

DEFINITION 1. Let x,y in Z^n. x moves outward to y if and only if y is
obtained by deleting the first coordinate of x and appending a new
coordinate of magnitude greater than all coordinates of x.

DEFINITION 2. Let F be any function. The F multiplicity of x on E is
the cardinality of the inverse image of F at x intersected with E. The
multiplicity can be infinite.

DEFINITION 3. The orthants of Z^n are the subsets of Z^n obtained by
imposing any set of n conditions +-x1 >= 0, ..., +-xn >= 0 on the
coordinates. Thus there are 2^n orthants in Z^n.

THEOREM 1. For every polynomial P:Z^n into Z^m, some x moves outward
to some y, where the F multiplicity of x is at most that of y on every
orthant in Z^n.

Note that because of infinite multiplicities, Theorem 1 is explicitly
Pi04. However, we can naturally make it explicitly Pi02 as follows.

DEFINITION 4. P:Z^n into Z^m is dominating if and only if for all x in
Z^n, the sup norm of x is at most the sup norm of P(x).

 THEOREM 2. For every dominating polynomial P:Z^n into Z^m, some x
moves outward to some y, where the F multiplicity of x is at most that
of y on every orthant in Z^n.

THEOREM 3. For any fixed n, Theorems 1,2 are provable in PA. Theorem 2
is provably equivalent to 1-Con(PA) over EFA. Theorem 1 implies
1-Con(PA) over EFA and follows from 2-Con(PA) over EFA.

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

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 923rd 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  Sun 1/9/22  6:57 PM
922: WQO Games  1/10/22 05:32:47 EST 2022

Harvey Friedman