921: Polynomials and PA/2

[Harvey Friedman]

We give some additional PA Incompleteness involving polynomials with
integer coefficients. These are arguably yet more natural.

This and the previous 920: Polynomials and PA are closely related to

https://www.ams.org/journals/proc/2016-144-02/S0002-9939-2015-12759-1/S0002-9939-2015-12759-1.pdf

There you will find some novel infinitary combinatorics leading to a
Pi11 sentence equivalent to epsilon_0 is well ordered. Finite forms
using >> are given to yield Pi02 statements equivalent to 1-Con(PA).

Here we derive arithmetic consequences of the Pi11 sentence by a
different method. We replace the infinitary functions there by
polynomials with integer coefficients from Z^n into Z^m. Shifting from
N to Z creates some very manageable complications.

It was already clear in that paper that we can replace infinitary
functions there by recursive, primitive recursive, elementary
recursive, or even lower, functions and also get arithmetic
statements.

These algebraic forms have the advantage that there is no
"sufficiently large" condition needed, and also we are restricting to
a particularly mainstream mathematical notion - integral polynomials.

TWO RELATIONS ON Z^n

We say that x,y in Z^n are lifting outward if and only if in each
coordinate, y is of the same sign (-,0,+) and magnitude at least that
of x.

We say that x,y in Z^n are moving outward if and only if y is obtained
by deleting the first term of x and adding a new term at the end of x
that has strictly greater magnitude than all terms in x,y.

THEOREM 1. Every surjective polynomial P:Z^n into Z^m sends some two
arguments lifting outward to two values moving outward.

Note that Theorem 1 is explicitly Pi03.

DEFINITION. P:Z^n into Z^m is dominating if and only if the sup norm
of every argument is at most the sup norm of its value.

THEOREM 2. Every dominating surjective polynomial P:Z^n into Z^m sends
some two arguments lifting outward to two values moving outward.

Note that Theorem 2. is explicitly Pi02.

THEOREM 3. Theorem 1 is provably equivalent to 2-Con(PA) over EFA.
Theorem 2 is provably equivalent to 1-Con(PA) over EFA.

Fix n,m, Note that going outward and moving outward are both examples
of integer piecewise linear relations as subsets of Z^n+m. And even
special ones at that. They are intersections of linear inequalities
with coefficients from -1,0,1.

TEMPLATE. Let n,m and integral piecewise linear R,S contained in Z^n x
Z^m = Z^n+m be given. Does every (dominating) surjective polynomial
P:Z^n into Z^m send some two R related arguments to two S related
values?

CONJECTURE. The status of every instance of the Template is
algorithmically decidable. Statements are either refutable in EFA or
provable in PA. The statements are well ordered under consistency
strength or interpretation power.

Alternatives in the Template are to use intersections of linear
inequalities with coefficients from -1,0,1, or to expand the Template
and use Presburger R,S. We make the same Conjecture if Presburger is
used.

This Template approach makes perfectly good sense also for the purely
combinatorial versions of what we are doing presented in
https://www.ams.org/journals/proc/2016-144-02/S0002-9939-2015-12759-1/S0002-9939-2015-12759-1.pdf

There we worked entirely on N, and here we work entirely on Z, and so
the two relations that we use are adjusted accordingly.

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

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 921st 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

Harvey Friedman