847: Brand New Tangible Incompleteness/5

[Harvey Friedman]

Recall our lead statement:

LEAD. Every order invariant subset of Q[-n,n]^k has a completely USH/N
invariant maximal square.

DEFINITION 1. W1 is the set of sentences obtained by fixing k in the
LEAD. W2 is the set of sentences obtained by fixing n in the LEAD. W3
is the set of sentences obtained by fixing both k,n in the LEAD.

THEOREM 1. All sentences in W1, W2, W3 are provable in SRP. For all r
and 1 <= i <= 3, Wi has an element provably equivalent over WKL0 to
Con(r-SRP).

CONJECTURE. W1 union W2 union W3 forms a set of sentences which is of
type omega under relative provability over RCA0.

We now go back to the LEAD and quantify over k,n, but consider choices
of natural functions from Q* into Q* other than USH/N.

DEFINITION 2. x,y in Q* are order,N equivalent if and only if x,y are
order equivalent and for all i, x_i in N iff x_j in N.

DEFINITION 3. f:Q* into Q* is an order,N invariant shift if and only
if for all order,N equivalent x,y in Q*, f(x)-x and f(y)-y is the same
tuple in {0,1}*,

USH/N is of course order,N invariant. Which order,N invariant f:Q*
into Q* can be used in LEAD?

DEFINITION 4. f:Q* into Q* is an admissible shift if and only if f:Q*
into Q* is an N,order invariant shift which is order preserving and
shifts only nonnegative integers. I.e., each f(x) is order equivalent
to x, and if f(x)_i = x_i + 1 then x_i in N.

Obviously USH/N:Q* into Q* is an admissible shift.

THEOREM 2. (RCA0) If some admissible shift f actually shifts the i-th
coordinate of x, then USH/N does. This characterizes USH/N among the
admissible shifts uniquely.

THEOREM 3. An order,N invariant shift f:Q* into Q* is usable in LEAD
if and only if it is admissible.

Theorem 3 is provably equivalent to Con(SRP) over WKL0.  The necessity
of admissibility is provable in RCA0.

It is obvious what we mean by f:Q^k into Q^k being an order,N
equivalent shift and being an admissible shift. For fixed k, there are
only finitely many order,N equivalent shifts from Q^k into Q^k.

DEFINITION 5. W[k,n] is the set of sentences obtained from the LEAD by
fixing k,n, and using any order,N equivalent shift from Q^k into Q^k
for USH/N. W[k] is the same as W[k,n] except n is quantified.

THEOREM 4. Every sentence in W[k,n] union W[k] is either provable in
SRP or refutable in RCA0, according to admissibility. For all r,
W[k,n] and W[k] have elements provably equivalent to Con(SRP[r]) over
WKL0.

CONJECTURE. W[k,n] union W[k] consists of implicitly Pi01 sentences
that are well ordered under relative provability over RCA0. The
relative provability is algorithmically solvable. Among the elements
are sentences provably equivalent over RCA0 to Con(PA_r), Con(PA),
Con(Z_r), Con(WZC), Con(ZFC), Con(MAH[r]), Con(SRP[r]), and just about
all of the commonly considered set theories below SRP.

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

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

Harvey Friedman