[FOM] 560: New Pi01/better

Mon Nov 3 19:45:47 EST 2014

THIS POSTING IS SELF CONTAINED

1. SMAH (reworking #558)
2. SRP
3. HUGE

1. SMAH (reworking #558).

We continue from #558
http://www.cs.nyu.edu/pipermail/fom/2014-October/018357. We start with
an improved version of #558.

All lower case letters represent positive integers unless indicated otherwise.

DEFINITION 1. Let R containedin N^2k = N^k x N^k. x red y if and only
if x,y in N^k, x R y, and max(x) > max(y). S containedin N^k is
irreducible if and only if there is no x red y, x,y in S. A red B if
and only if  A,B are subsets of N, where every element of A^k\S
reduces to an element of B^k intersect S.

BACKGROUND. Every R containedin N^2k has a unique irreducible S for
which N red N. S is called the basis for R.

Weak bases arise if we have an irreducible S for which, say, A red B
red C red D, for various choices of A,B,C,D containedin N.

TEMPLATE. Every R contained in N^2k has an irreducible S for which
some infinite A red B red C red N obeys a given Boolean equation in
A,B,C,A+1,B+1,C+1.

PROPOSITION 1.1. Every R containedin N^2k has an irreducible S for
which some infinite A red B red C red N has B+1 containedin C\A.

To get a simple explicitly Pi01 form of Proposition 1.1, we need to
move to order invariant R. It should be noted that if we are going to
move to order invariant R, we also have the alternative Proposition
2.1.

PROPOSITION 1.2. Every order invariant R containedin N^2k has an
irreducible S for which some infinite A red B red C red N has B+1
containedin C\A.

PROPOSITION 1.3. Every order invariant R containedin N^2k has an
irreducible S for which some (8kN)! red B red C red N has B+1
containedin C\(8kN)!.

PROPOSITION 1.4.  Every order invariant R containedin [t]^2k has an
irreducible S for which some  (8kN)! intersect [t] red B red C red [t]
has B+1 containedin C\(8kN)!.

Here [t] = {1,...,t}.

THEOREM 1.5. Propositions 1.1-1.4 are provably equivalent to Con(SMAH)
over ACA. Proposition 1.4 is explicitly Pi01.

2. SRP

We will work with order invariant R containedin [t^t]^2k. We also will
be using a second relation T containedin N^2k.

DEFINITION 2.1. Let S containedin [t^t]^k. t<S> is the set of all
elements of [t^t]^k which are obtained by multiplying all coordinates
>= t of some element of S by t.

NOTE: This notion sometimes is referred to as "invariant" or
"completely invariant" by some authors.

PROPOSITION 2.1. Every order invariant R containedin [t^t]^2k, t
>(8k)!, has an irreducible S containing t<S> for which some
{1,t,t^2,...,t^t} red A red [t^t].

There is a stronger form of Proposition 2.1 using stability.

DEFINITION 2.2. Let E containedin [t^t]^k and f be a function. E is f
stable if and only if for all x,f(x) in [t^t]^k, x in E iff f(x) in E.

DEFINITION 2.3. t-um is the function from [t^t]^k into N^k, where
t-um(x) is the result of multiplying all coordinates of x that are >=
t by t. Here "um" is read "upper multiplication".

PROPOSITION 2.2. Every order invariant R containedin [t^t]^2k, t
>(8k)!, has a t-um stable irreducible S for which some
{1,t,t^2,...,t^t} red A red [t^t].

Propositions 2.1 and 2.2 are explicitly Pi01.

THEOREM 2.3. Propositions 2.1 and 2.2 are provably equivalent to
Con(SRP) over EFA = exponential function arithmetic.

3.  HUGE

We now come to HUGE. For this, we make a small modification in the
notion of reduction, use t<S>, and add a cross section condition.

DEFINITION 3.1. Let R containedin [t^t]^2k. x red* y if and only if
x,y in N^k, x R y and max(x) >  x_1 > max(y). S containedin [t^t]^k is
irreducible* if and only if there is no x red* y, x,y in S. A red* B
if and only if  A,B are subsets of N, where every element of A^k\S
reduces* to an element of B^k intersect S.

Firstly, this change in reducibility does not affect the status of
Propositions 2.1, 2.2.

PROPOSITION 3.1. Every order invariant R containedin [t^t]^2k, t
>(8k)!, has an irreducible* S containing t<S> for which some
{1,t,t^2,...,t^t} red* A red* [t^t].

PROPOSITION 3.2. Every order invariant R containedin [t^t]^2k, t
>(8k)!, has a t-up stable irreducible* S for which some
{1,t,t^2,...,t^t} red* A red* [t^t].

DEFINITION 3.2. Let S containedin [t^t]^k. S[n] = {m: (n,...,n,m) in S}.

PROPOSITION 3.3. Every order invariant R containedin [t^t]^2k, t >
(8k)!, has a t-um stable irreducible* S, each S[2t^i] = [2t^i]
intersect tN, for which some {1,t,t^2,...,t^t} red* A red* [t^t].

Note that Propositions 3.1 - 3.3 are explicitly Pi01.

THEOREM 3.3. Propositions 3.1 and 3.2 are provably equivalent to Con(SRP) over
EFA. Proposition 3.3 is provably equivalent to Con(HUGE) over EFA.

************************************************************
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 560th 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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html

528: More Perfect Pi01  8/16/14  5:19AM
529: Yet more Perfect Pi01 8/18/14  5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01  8/22/14  5:16PM
532: More General Theory/Perfect Pi01  8/23/14  7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14  1:17AM
534: Perfect Explicitly Pi01  8/27/14  10:40AM
535: Updated Perfect Explicitly Pi01  8/30/14  2:39PM
536: Pi01 Progress  9/1/14 11:31AM
537: Pi01/Flat Pics/Testing  9/6/14  12:49AM
538: Progress Pi01 9/6/14  11:31PM
539: Absolute Perfect Naturalness 9/7/14  9:00PM
540: SRM/Comparability  9/8/14  12:03AM
541: Master Templates  9/9/14  12:41AM
542: Templates/LC shadow  9/10/14  12:44AM
543: New Explicitly Pi01  9/10/14  11:17PM
544: Initial Maximality/HUGE  9/12/14  8:07PM
545: Set Theoretic Consistency/SRM/SRP  9/14/14  10:06PM
546: New Pi01/solving CH  9/26/14  12:05AM
547: Conservative Growth - Triples  9/29/14  11:34PM
548: New Explicitly Pi01  10/4/14  8:45PM
549: Conservative Growth - beyond triples  10/6/14  1:31AM
550: Foundational Methodology 1/Maximality  10/17/14  5:43AM
551: Foundational Methodology 2/Maximality  10/19/14 3:06AM
552: Foundational Methodology 3/Maximality  10/21/14 9:59AM
553: Foundational Methodology 4/Maximality  10/21/14 11:57AM
554: Foundational Methodology 5/Maximality  10/26/14 3:17AM
555: Foundational Methodology 6/Maximality  10/29/14 12:32PM
556: Flat Foundations 1  10/29/14  4:07PM
557: New Pi01  10/30/14  2:05PM
558: New Pi01/more  10/31/14 10:01PM
559: Foundational Methodology 7/Maximality

Harvey Friedman