926: Polynomials and PA/6

[Harvey Friedman]

In 925: Polynomials and PA/5 I wrote

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

There is a small typo there. This should read

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 such that each
#(P_i,x_1,...,x_m) <= #(P_i,x_2,...,x_m+1).

We want to redesign the Template as follows.

TEMPLATE. Let R be a binary relation on Z^m which is a subset of Z^2m
definable over (Z,<) with parameters allowed. Let P_1,...,P_r:Z^n into
Z^m be (dominating) integral
polynomials. There exists x R y 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 each should have 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 926th 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
925: Polynomials and PA/5

Harvey Friedman