# [FOM] 594: Finite Continuation Theory 13/perfect?

Harvey Friedman hmflogic at gmail.com
Tue Aug 4 13:44:02 EDT 2015

```We now see what happens when we replace the rationals with the reals = R.

Recall the perfect Proposition A from

http://www.cs.nyu.edu/pipermail/fom/2015-July/018859.html

PROPOSITION A. Every finite subset of Q^k|>n has a maximal nonnegative
continuation, where S_1...n|>n = S_0...n-1|>n.

PROPOSITION A (reals). Every finite subset of R^k|>n has a maximal nonnegative
continuation, where S_1...n|>n = S_0...n-1|>n.

Because of the Upward Skolem Lowenheim theorem, we also see that
Proposition A (reals) is implicitly Pi01, and provably equivalent,
over ZC, to Con(SRP).

However, with Proposition A, the maximal nonnegative continuation can
be taken to be arithmetical, in fact delta-0-2. What can we say of
this kind for Proposition A (reals)? Can we take the maximal
nonnegative continuation to be Borel? I doubt it, but I need to look
further.

THEOREM 1. Proposition A (reals)  is provably equivalent to Con(SRP) over ZC.

HOWEVER, now let us look at the new finite forms Propositions B,C of
http://www.cs.nyu.edu/pipermail/fom/2015-July/018859.html

PROPOSITION B. Let E be an equivalence relation on Q^k
with finitely many equivalence classes. Every finite subset of Q^k|>n
has a finite E-maximal nonnegative continuation, where S_1...n|>n =
S_0...n-1|>n.

PROPOSITION C. Let E be an order theoretic equivalence relation on Q^k
with finitely many equivalence classes. Every finite subset of Q^k|>n
has a finite E-maximal nonnegative continuation, where S_1...n|>n =
S_0...n-1|>n.

On the reals:

PROPOSITION B (reals). Let E be an equivalence relation on R^k
with finitely many equivalence classes. Every finite subset of R^k|>n
has a finite E-maximal nonnegative continuation, where S_1...n|>n =
S_0...n-1|>n.

PROPOSITION C (reals). Let E be an order theoretic equivalence relation on R^k
with finitely many equivalence classes. Every finite subset of R^k|>n
has a finite E-maximal nonnegative continuation, where S_1...n|>n =
S_0...n-1|>n.

Proposition C (reals) is explicitly Pi02 given the usual decision
procedure for dense linear orderings. With an easy a priori upper
bound on the size of the finite E-maximal nonnegative continuation, it
is put in explicitly Pi01 form. In fact, we can also go pretty
directly from Proposition C to Proposition C (reals) and back.

THEOREM 2. Proposition B (reals) is provably equivalent to Con(SRP)
over Z. Proposition C (reals) is provably equivalent to Con(SRP) over
RCA0.

************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
This is the 594th 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
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/27/15  10:39 AM
577: New Pi01 Incompleteness  3/7/15  2:54PM
578: Provably Falsifiable Propositions  3/7/15  2:54PM
579: Impossible Counting  5/26/15  8:58PM
580: Goedel's Second Revisited  5/29/15  5:52 AM
581: Impossible Counting/more  6/2/15  5:55AM
582: Link+Continuation Theory  1  6/21/15  5:38PM
583: Continuation Theory 2  6/23/15  12:01PM
584: Finite Continuation Theory 3   6/26/15  7:51PM
585: Finite Continuation Theory 4  6/29/15  11:23PM
586: Finite Continuation Theory 5  6/20/15  1:32PM
587: Finite Continuation Theory 6  7/1/15  11:39PM
588: Finite Continuation Theory 7  7/2/15  2:44PM
589: Finite Continuation Theory 8  7/4/15  6:51PM
590: Finite Continuation Theory 9  7/6/15  5:20PM
591: Finite Continuation Theory 10  7/12/15  3:38PM
592: Finite Continuation Theory 11/perfect?  7/29/15  4:30PM
593: Finite Continuation Theory 12/perfect?  8/23/15  9:47PM

Harvey Friedman
```