920: Polynomials and PA

Harvey Friedman hmflogic at gmail.com
Fri Jan 7 00:16:35 EST 2022


DEFINITION 1. n in Z points outward to m in Z if and only if |n| <=
|m| and n,m have the same sign (+,-,0). x in Zk points outward to y in
Zk if and only if each xi points outward to yi. A containedin Z^k
points outward to B containedin Z^k if and only if every element of A
points outward to some element of B.

DEFINITION 2.  The fiber of P:Z^k into Z^k at x is the set of all y
such that P(y) = x and the sup norm of y is at most the sup norm of x.
The bounded fiber of P:Z^k into Z^k at x is the set of all y such that
P(y) = x and the sup norm of y is at most the sup norm of x.

THEOREM 1. For all polynomials P"Z^k into Z^k with integer
coefficients, there exists integers 0 < a_1 < ... < a_k+1 such that
the fiber of P at (a_1,...,a_k) points outward to the fiber of P at
(a_2,...,a_k+1).

THEOREM 2. For all polynomials P"Z^k into Z^k with integer
coefficients, there exists integers 0 < a_1 < ... < a_k+2 such that
the cardinality of the fiber of P at (a_1,...,a_k) is at most the
cardinality of the fiber of P at (a_2,...,a_k+1) is at most the
cardinality of the fiber of P at (a_3,...,a_k+2).

THEOREM 3. For all polynomials P"Z^k into Z^k with integer
coefficients, there exists integers 0 < a_1 < ... < a_k+1 such that
the bounded fiber of P at (a_1,...,a_k) points outward to the bounded
fiber of P at (a_2,...,a_k+1).

THEOREM 4. For all polynomials P"Z^k into Z^k with integer
coefficients, there exists integers 0 < a_1 < ... < a_k+2 such that
the cardinality of the bounded fiber of P at (a_1,...,a_k) is at most
the cardinality of the bounded fiber of P at (a_2,...,a_k+1) is at
most the cardinality of the bounded fiber of P at (a_3,...,a_k+2).

THEOREM 5. Theorems 1,2 are provably equivalent to 2-Con(PA) over EFA.
Theorems 3,4 are provably equivalent to 1-Con(PA) over EFA.
Obvious numerical functions associated with Theorem 1 eventually
dominate all <epsilon_0 recursive functions, but are epsilon_0
recursive.

With Theorem 1, I use a (weak form of a) recent result of
https://arxiv.org/abs/1909.06719

How does this compare to other PA incompleteness? This does have some
advantages.

1. It is already explicitly Pi02 as written (except Theorems 1,2 are
explicitly Pi04).
2. The input is integral polynomials, one of the most natural of all notions.
3. Inverse images of points are very standard.
4. Pointing outward for numbers, tuples, and sets of tuples, is very
natural and visual.

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

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

Harvey Friedman


More information about the FOM mailing list