924: Polynomials and PA/4

[Harvey Friedman]

DEFINITION 1.. Let x,y in Z^m. x <* y if and only if y is obtained
from x by deleting the first coordinate and appending a last term of
magnitude greater than all coordinates of x,y.

DEFINITION 2. Let F be any function. #(P,x) is the cardinality of the
preimage of x under P. This is "multiplicity".

DEFINITION 3. P:Z^n into Z^m is dominating if and only if each x in
Z^n has sup norm at most that of P(x).

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).

Note that Theorem 1 with dominating is explicitly Pi02, whereas
Theorem 1 without dominating is explicitly Pi04.

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

THEOREM 3. Theorem 1 without "dominating" is provable in EFA +
2-Con(PA). Theorem 1 with r = 1 and s = 2 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 = s = 2 or
even if we set r = 1 and s = 3.

There appears to be an obvious Template Challenge here.

TEMPLATE. Let n,m,r,s be given. Let R be a relation on Z^m. Does
Theorem 1 hold universally?

This is rather crude because we place no condition on R.

DEFINITION 4. x,y in Z^m are sign order equivalent if and only if for
all 1 <= i,j <= m, x_i < x_j iff y_i < y_j, and the sign of x_i
(+,-,0) equals the sign of x_j (+,-,0). E contained in Z^m is sign
order invariant if and only if for all sign order equivalent x,y in
Z^m, x in E iff y in E.

PROPOSITION. <*.on Z^m is a sign order invariant relation on Z^m.
Moreover, the "adjacency relation" used in
https://www.ams.org/journals/proc/2016-144-02/S0002-9939-2015-12759-1/S0002-9939-2015-12759-1.pdf
is also sign order invariant.

RESEARCH.
1. For which order invariant relations on N^m does the Template hold?
2. For which signed order invariant relations on Z^m does it hold?
3. For which integral piecewise linear relations on Z^m does it hold?
4. For which Presburger relations on Z^m does it hold?

It is clear that these cannot be solved in PA, and it is purely
arithmetical (with or without "dominating"). We conjecture that there
is a low level even understandable algorithm for even 4 which
provably works just beyond PA, and in each fixed dimension, provably
works in PA. Also if an instance is false then it is refutable in EFA.

One should have well orderedness under logical strength and
interpretation power, and if we use only dominating we should get well
orderedness under logical implications over EFA, and if we don't use
dominating we should also get well orderedness under logical
implications over EFA.

This should add to the growing examples of
statements from nature that are well ordered or at least comparable
under interpretation power and more.

This approach would appear to be far more promising on several fronts
than any other approaches to PA Incompleteness thus far. However it
does not yet appear to be relevant to the realm of stronger forms of
Incompleteness.

I should mention that these PA Incompleteness results depend heavily on MRDP.

I would welcome opinions as to how this compares with other examples
of PA Incompleteness?

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

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 924th 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