[FOM] 577: New Pi01 Incompleteness

[Harvey Friedman]

We have previously given "perfect" implicitly Pi01 incompleteness
using maximal squares (roots, cliques) and projections. See
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87. Here are two samples.

PROPOSITION. Every order invariant subset of Q[0,1]^k has a maximal
square whose projections at equal length subsequences of 1,1/2,...,1/k
agree below 1/k.

PROPOSITION. Every order invariant subset of Q[0,1]^2k has a maximal
root whose projections at equal length subsequences of 1,1/2,...,1/n
agree below the min of their collective terms.

I now think of the first of these two as the leadoff perfect statement.

There are a lot of variants involving graphs and cliques instead of
maximal squares and maximal roots, fixed small dimensions, additional
parameter for length of subsequences, and consecutive terms. These
statements are all implicitly Pi01 via straightforward applications of
Goedel's completeness theorem. They are all provably equivalent to
Con(SRP) over WKL_0. I regard them as perfect, in a sense that has yet
to be seriously analyzed.

We have another kind of perfect implicitly Pi01 incompleteness, this
time using bases and upper shifts (explained below). This is an
improved version of an earlier statement.

PROPOSITION 2.2. In every order invariant relation on Q^k, some basis
of some (E union {0})^k contains its upper shift.

By an application of Goedel's completeness theorem, this also can be
seen to be implicitly Pi01. We also get provable equivalence with
Con(SRP) over WKL_0. Here there are few competitive variants. Most
notably, we can fix a small k, and still obtained equivalence with
Con(SRP).

The biggest recent advance relates to the quest for EXPLICITLY Pi01
incompleteness. Here we have a major advance toward perfection.

PROPOSITION 4.1. In every order invariant relation on Q^k, some
nonempty finite set, point reducing its nonempty finite
{0,...,k}-images, is free with its upper shift.

The above is obviously explicitly finite. It can be construed as Pi01
first by bounding the cardinality of the set and then using well known
facts about the first order theory of (Q,<). For an explicitly Pi01
form, we use {0,...,k}-coordinate images. It is easily seen that the
finite {0,...,k}-images and the {0,...,k}-coordinate images of a
finite set are the same.

PROPOSITION 5.3. In every order invariant relation on Q^k, some
nonempty finite subset of Q[(8k)!)]^k, point reducing its nonempty
{0,...,k}-coordinate images, is free with its upper shift.

Proposition 5.3 is explicitly Pi01.

As usual, we work with order invariant relations on Q^k, which are
order invariant subsets of Q^2k. We will also work with order
theoretic relations with parameters 0,...,k that are subsets of
(Q^k)^k x Q^k. Recall that for fixed k, there are only finitely many
such.

1. Bases and Upper Shifts.
2. Implicitly Pi01 Incompleteness.
3. Reductions and Principal Images.
4. Explicitly Finite Incompleteness.
5. Explicitly Pi01 Incompleteness.
6. Extreme Implicitly Pi01 Incompleteness.
7. Further Considerations.

1. BASES

DEFINITION 1.1. Let R be a relation on Q^k. x strictly reduces to y if
and only if x R y and max(x) > max(y). S is a basis for E if and only
if E containedin Q^k and S = {x in E: x does not strictly reduce to
any y in S}.

DEFINITION 1.2. The upper shift of x in Q^k is the result of adding 1
to all nonnegative coordinates of x. The upper shift of S containedin
Q^k is the set of all upper shifts of elements of S.

2. IMPLICITLY Pi01 INCOMPLETENESS

THEOREM 2.1. In every relation on Q^k, every subset of Q^k with a well
ordered set of coordinates has a unique basis.

PROPOSITION 2.2. In every order invariant relation on Q^k, some basis
of some (E union {0})^k contains its upper shift.

There is a nice way to use Goedel's Completeness Theorem to see that
Proposition 2.2 is implicitly Pi01.

THEOREM 2.3. Proposition 2.2 is provably equivalent to Con(SRP) over WKL_0.

3. REDUCTIONS AND X-IMAGES

DEFINITION 3.1. Let R be a relation on Q^k. x reduces to y if and only
if x = y in Q^k or x strictly reduces to y.  S point reduces T if and
only if S,T containedin Q^k and some element of T reduces to some
element of S.

DEFINITION 3.2. Let R be a relation on Q^k. S is free if and only if S
containedin Q^k and no element of S strictly reduces to an element of
S. S is free with T if and only if S union T is free.

DEFINITION 3.3. The X-images of S containedin Q^k are the images of
S^k under order theoretic R containedin (Q^k)^k x Q^k with parameters
from X.

4. EXPLICITLY FINITE INCOMPLETENESS

PROPOSITION 4.1. In every order invariant relation on Q^k, some
nonempty finite set, point reducing its nonempty finite
{0,...,k}-images, is free with its upper shift.

THEOREM 4.2. Proposition 4.1 is provably equivalent to Con(SRP) over EFA.

Proposition 4.1 is obviously explicitly finite, We can put Proposition
4.1 in Pi01 form by the following considerations. First observe that
if S obeys the conclusion, then there is an S' containedin S obeying
the conclusion, with cardinality bounded by an exponential expression
in k. Next observe finite {0,...,k}-images of S' must use only
coordinates of elements of S' and 0,...,k. From these observations,
for each k, the conclusion is a corresponding first order sentence in
(Q,<) with parameters 0,...,k. From elimination of quantifiers in
(Q,<), we have put Proposition 4.1 in Pi01 form.

5. EXPLICITLY Pi01 INCOMPLETENESS

DEFINITION 5.1. Let S containedin Q^k. The X-coordinate images of S
are the X-images V of S^k such that every coordinate of any element of
V is a coordinate of some element of S or an element of X

Definition 5.1 is used only to obtain explicit Pi01 incompleteness. It
is easily seen that the finite X-images are the same as the
X-coordinate images (assuming S is finite).

PROPOSITION 5.1. In every order invariant relation on Q^k, some
nonempty finite set, point reducing its nonempty {0,...,k}-coordinate
images, is free with its upper shift.

PROPOSITION 5.2. In every order invariant relation on Q^k, some
nonempty finite sett with at most (8k)! elements, point reducing its
nonempty {0,...,k}-coordinate images, is free with its upper shift.

Propositions 5.1, 5.2 are explicitly Pi02. Proposition 5.2 is Pi01 via
immediate use of elimination of quantifiers for (Q,<).

DEFINITION 5.2. Q[n]  is the set of fractions whose numerator and
denominator are of magnitude at most n.

PROPOSITION 5.3. In every order invariant relation on Q^k, some
nonempty finite subset of Q[(8k)!)]^k, point reducing its nonempty
{0,...,k}-coordinate images, is free with its upper shift.

Proposition 5.3 is explicitly Pi01.

THEOREM 5.4. Propositions 5.1 - 5.3 are provably equivalent to
Con(SRP) over EFA.

6. EXTREME IMPLICITY Pi01 INCOMPLETENESS

DEFINITION 6.1. Let S containedin Q^k and x in Q^k. S^<= = {x in S:
x_1 <= ... <= x_k}. The lower projections of S are the sets {x:
S(p,x): max(x) < p}, p in Q.

DEFINITION 6.2. Let R be a relation on Q^k. S is a <=-basis for E if
and only if S containedin E and S^<= = {x in E^<=: x does not reduce
to any y in S}.

PROPOSITION 6.1. In every order invariant relation on Q^k, for some
<=-basis of some (E union {0})^k, the elements and lower projections
include those of its upper shift.

There is a nice way to use Goedel's Completeness Theorem to see that
Proposition 6.1 is implicitly Pi01.

THEOREM 6.2. Proposition 6.1 is provably equivalent to Con(HUGE) over EFA.

7. FURTHER CONSIDERATIONS

In all Propositions mentioned here, we can require that the sets
claimed in the conclusion are either

i. Definable in (Q,<,N). This is the same as being arithmetical.
2. Recursive in 0'. This is the same as being delta-0-2.

If we make this requirement, then we get statements that are provably
equivalent to the original forms over ACA_0. This provides a
straightforward but not satisfactorily mathematical way of obtaining
explicitly finite Incompleteness.

************************************************************
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 577th 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  11/214  10:35PM
560: New Pi01/better  11/314  7:45PM
561: New Pi01/HUGE  11/5/14  3:34PM
562: Perfectly Natural Review #1  11/19/14  7:40PM
563: Perfectly Natural Review #2  11/22/14  4:56PM
564: Perfectly Natural Review #3  11/24/14  1:19AM
565: Perfectly Natural Review #4  12/25/14  6:29PM
566: Bridge/Chess/Ultrafinitism 12/25/14  10:46AM
567: Counting Equivalence Classes  1/2/15  10:38AM
568: Counting Equivalence Classes #2  1/5/15  5:06AM
569: Finite Integer Sums and Incompleteness  1/515  8:04PM
570: Philosophy of Incompleteness 1  1/8/15 2:58AM
571: Philosophy of Incompleteness 2  1/8/15  11:30AM
572: Philosophy of Incompleteness 3  1/12/15  6:29PM
573: Philosophy of Incompleteness 4  1/17/15  1:44PM
574: Characterization Theory 1  1/17/15  1:44AM
575: Finite Games and Incompleteness  1/23/15  10:42AM
576: Game Correction/Simplicity Theory 1  1/27/15 10:39AM

Harvey Friedman