[FOM] 538: Progress Pi01

[Harvey Friedman]

http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82 - #84 are fully operational.

#82,#84 are frequently being updated, although we expect most of the
updates going forward to be for #82.

We have been seeing what additional simplifications can be made if we
maximize solutions to purely universal conditions, rather than
maximize squares, roots, and cliques. Thus in these versions, we are
using stronger hypotheses, and so we are able to get simpler
conclusions - for independence from ZFC.

PROPOSITION 1. Every purely universal condition on subsets of
Q[-n,n]^k has a maximal solution whose sections at (0,...,n-1) and
(1,...,n) have the same negative part.

PROPOSITION 2. Every purely universal condition on regressive partial
f:Q[-k,k]^k into Q[-k,k]^k has a maximal solution with f(0,...,k-1) ==
f(1,...,k).

Here == means "both sides are equal or both sides are undefined".
Recall that a purely universal condition is a universally quantified
Boolean combination of inequalities in just <, without constants.

THEOREM 3. Propositions 1,2 are provably equivalent to Con(SRP) over WKL_0.

****************************************
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 538th 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

Harvey Friedman