851: Product Inequality Theory/1

Wed Apr 29 00:08:57 EDT 2020

We now move over to functions. Overall this seems to be working better
than Set Equation Theory/3,
https://cs.nyu.edu/pipermail/fom/2020-April/022125.htm There is a big
advantage for explicitly Pi01 forms. The set approach requires towers,
whereas the function approach does not.

However, the Set Equation approach still has enough independent merits
that I do not consider it being obsoleted by this Product iInequality
approach.

We work with binary operations dot:A^2 into A, where N containedin A
contianedin Q.

We use terms in dot and variables. usually with no constants allowed.
The degree is the number of occurrences of variables. Terms are
analogous to polynomials in algebra with no constants. In addition we
use terms with if then else using < between terms. These are called
Piecewise Poly Terms, and are in analogy with piecewise polynomials
with no constants.

DEFINITION 1. Q,Z.Z+,N are the set of all rationals, integers,
positive integers, and nonnegative integers, respectively. We use
a,b,c,d,e,p,q,r,s for rationals, and k,n,m for positive integers,
unless indicated otherwise. The upper shift is defined by ush(p) = p
if p < 0; p+1 otherwise. ush(p,q,r) = (ush(p),ush(q),ush(r)).

THEOREM 1. Let t be a poly term in variables p,q,r, and A be a well
ordered subset of Q containing N. There is a unique dot:A^2 into A
such that for all r <= max(p,q) from A,
t(p,q,p dot q) <= t(p,q,r)..

PROPOSITION 2. Let t be a piecewise poly term in variables p,q,r.
There is a dot:A^2 into A, N containedin A containedin Q, such that
for all r <= max(p,q) from A,
t(p,q,p dot q) <= t(p,q,r) <= t(ush(p,q,r)).

PROPOSITION 3. Let t be a piecewise poly term in variables p,q,r.
There is a dot:A^2 into A, N containedin A containedin Q, such that
for all p,r <= q f< j from A,
t(p,q,p dot q) <= t(p,q,r) <= t(ush(p,q,r)) = t(j dot p,j dot q,j dot r).

THEOREM 4. Proposition 2 is provably equivalent to Con(SRP) over
WKL_0, where the implication to Con(SRP) is provable in RCA_0.
Proposition 3 is provably equivalent to Con(huge) over WKL_0, where
the implication to Con(HUGE) is provable in RCA_0.

*EXPLICITLY Pi01 STATEMENTS*

For this, it is natural to shift from the rationals to the integers.
First we make a very general definition.

DEFINITION 2. Let dot:A^2 into A where a1,...,am lie in A.
GEN(k;a1,...,an) is the set of values of poly terms of length <= k
with variables replaced by various of the a1,...,an.

THEOREM 5. Let t be a piecewisepoly term in variables p,q,r. There is
a dot:{-kn,...,kn}^2 into {-kn,...,kn} such that for all r <= max(p,q)
from {-kn,...,kn},
t(p,q,p dot q) <= t(p,q,r).

PROPOSITION 6. Let t be a piecewise poly term in variables p,q,r of
degree d, and n >> d,k. There is a dot:{-kn,...,kn}^2 into
{-kn,...,kn} such that for all r <= max(p,q) in GEN(k;0,n,...,kn),
t(p,q,p dot q) <= t(p,q,r) <= t(ush/n(p,q,r))

PROPOSITION 7. Let t be a piecewise poly term in variables p,q,r and n
>> d,k. There is a dot:{-kn,...,kn}^2 into {-kn,...,kn} such that for
all r <= max(p,q) in GEN(k;0,n,...,kn),
t(p,q,p dot q) <= t(p,q,r) <= t(ush/n(p,q,r)) <= t(jk dot p,jk dot q,jk dot r).

THEOREM 8. Proposition 6 is provably equivalent to Con(SRP) over EFA.
Proposition 7 is provably equivalent to Con(HUGE) over EFA. These
results hold if n >> d,k is replaced by n > (8dk)!!.

TEMPLATES

There are an incredibly rich opportunities for interesting Templates
here, even for the trivially provable Theorems 1,5. E.g., look at

t(alpha,beta,gamma) <= t(alpha',beta',gamma'),

still using r <= max(p,q), and taking
alpha,beta,gamma,alpha',beta',gamma' from the variables p,q,r and all
nine products of length 2 of p,q,r. Obviously endless more tiny
templating like this for 2,3,6,7.

COMPUTER INVESTIGATIONS

5,6,7 suggest starting with various small piecewise poly terms and
looking for associated binary products. If we fail to find a
corresponding dot thru exhaustive search then we have refuted SRP or
HUGE. Otherwise, if we find a corresponding product, depending on
details, we can argue that we have made a confirmation. A lot of work
may be needed to keep such computations from blowing up even with a
very small piecewise poly term.

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

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 851st 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM

Harvey Friedman