[FOM] 640: Progress in Pi01 Incompleteness 3

Fri Oct 30 15:30:41 EDT 2015

THIS POSTING IS SELF CONTAINED

First we correct a typo from
http://www.cs.nyu.edu/pipermail/fom/2015-October/019304.html  I wrote

PROPOSITION 1.4. Every order invariant relation on Q^k has a step
maximal root, where for all order equivalent x,y in N^k, S[x]|<min(xy)
= S[y]|<min(xy).

This should be

PROPOSITION 1.4. Every order invariant relation on Q^k has a step
maximal root, where for all order equivalent x,y in N*, S[x]|<min(xy)
= S[y]|<min(xy).

Here N* is the set of all finite tuples from N.

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

As promised in http://www.cs.nyu.edu/pipermail/fom/2015-October/019279.html
I continue with item 2 below. Item 1 was discussed in
http://www.cs.nyu.edu/pipermail/fom/2015-October/019304.html

To orient the reader, I again give a highly abridged version of
http://www.cs.nyu.edu/pipermail/fom/2015-October/019279.html

1. Order invariant relations and maximal roots. This yields implicitly
Pi01 for SRP. Uses order invariant relations.See
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87

2. Constrained Function Theory.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019253.html Here we
use PUD (purely universally definable) sets of partial functions, and
get implicitly Pi01 for SRP. The idea here is that any PUD set of
partial functions with an extension property (it's an r.e. condition)
has a very good element (satisfying certain equations).

3. Fixed Point Minimization.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019264.html Here we
obtain implicitly Pi01 for SRP and for HUGE. We also get explicitly
Pi01 for SRP and HUGE. Uses order invariant relations only, and not
PUD. Here the key idea is the natural notion of a fixed point
minimizer for a relation.

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

Here functions are introduced, as opposed to just sets in 1 above. 2
and 3 above differ in the use of partial functions in the former. My
present thinking is that the use of functions in 2 and 3 is the
preferred way to go when moving up to HUGE and also when going to the
explicitly Pi01.

CONSTRAINED FUNCTION THEORY
by
Harvey M. Friedman
October 27, 2015

1. PUD, upper shift, extensions
2. Embeddings

1. PUD, UPPER SHIFT, EXTENSIONS

DEFINITION 1.1. Q,Z+,N is the set of all rationals, positive integers,
nonnegative integers, respectively. We use n,m,r,s,t for positive
integers unless indicated otherwise. We use p,q for rationals. The
upper shift ush(x) of x in Q^k results from adding 1 to all
nonnegative coordinates of x. For E containedin Q^k,

DEFINITION 1.2. f::Q^k into Q^k if and only if f is a partial function
from Q^k into Q^k, where every coordinate of every value is a
coordinate of some argument. Let E containedin Q^k,  E|<p, E|<=p,
E|>p, E|>=p is the set of all xi in E such that max(x) is <p, <=p, >p,
>=p, respectively. x <= E if and only if x in Q^k and for all y in E,
max(x) >= max(y).

DEFINITION 1.3. A set V of f::Q^k into Q^k has the first extension
property if and only if any f in V can be extended at any x >= dom(f)
so that it remains in V. V has the second extension property if and
only if any f in V can be extended at any x >= dom(f)|>=0, to any
g::Q^k into Q^k, and remain in V.

DEFINITION 1.4. V is a PUD set of f::Q^k into Q^k if and only if E can
be defined as the set of all f::Q^k into Q^k such that (forall
x_1,...,x_r in dom(f))(phi), where phi is a propositional combination
of inequalities s < t, where s,t is a specific coordinate of some x_i
or f(x_i).

THEOREM 1.1. The two extension properties for PUD sets of f::Q^k into
Q^k are Sigma01; i.e., recursively enumerable (in presentations).

Theorem 1.1 is proved by the Goedel Completeness Theorem.

PROPOSITION 1.2. Every PUD set of f::Q^k into Q^k with the first
extension property (first and second extension properties) has an
f:D^k into D^k, 0 in D, with f(ush(x)) = ush(f(x)).

PROPOSITION 1.3. Every PUD set of f::Q^k into Q^k with the first and
second extension properties has an f:D^k into D^k, 0 in D such that
i. f(ush(x)) = ush(f(x)), x in D^k.
ii. f(k+.5,p,...,p) = (k,p+1,...,p+1), p in D intersect [0,k-1].

THEOREM 1.4. Proposition 1.2 is provably equivalent to Con(SRP) over
WKL_0. For some tiny fixed k, Proposition 1.2 is provably equivalent
to Con(SRP) over WKL_0. Proposition 1.3 is provably equivalent to
Con(HUGE) over WKL_0. For each fixed k, Proposition 1.3 is provable in
HUGE.

SRP = ZFC + {there exists a cardinal with the k-SRP}_k. SRP+ = ZFC +
(for all k there exists a cardinal with the k-SRP).

The SRP hierarchy of large cardinals is intertwined with the subtle
and ineffable cardinal hierarchies.

HUGE = ZFC + {there exists a nontrivial elementary embedding
j:V(lambda) into V(mu) such that j^(k)(kappa) exists}_k.

2. EMBEDDINGS

DEFINITION 2.1. Let E containedin Q^k. E is order theoretic if and
only if E can be defined by a propositional combination of
inequalities between variables x_1,...,x_k and constants from Q. h is
an embedding of E if and only if h::Q into Q, and for all x,hx in Q^k,
x in S iff hx in S. Here h acts coordinatewise.

TEMPLATE 2.1. Let partial h:Q into Q be order theoretic (piecewise
linear with rational coefficients, finitely many pieces). Every PUD
set of f::Q^k into Q^k with the first extension property has an h
embedded f:D^k into D^k, 0 in D.

TEMPLATE 2.2. Let partial h:Q into Q be order theoretic (piecewise
linear with rational coefficients). Every PUD set of f:::Q^k into Q^k
with the first and second extension property has an h embedded f:D^k
into D^k, 0 in D.

There are some more ambitious multiple forms of these Templates.

TEMPLATE 2.3. Let partial h_1,...,h_r:Q into Q be order theoretic
(piecewise linear with rational coefficients, finitely many pieces).
Every PUD set of f::Q^k into Q^k with the first extension property has
an h_1,...,h_r embedded f:D^k into D^k, 0 in D.

TEMPLATE 2.4. Let partial h_1,...,h_r:Q into Q be order theoretic
(piecewise linear with rational coefficients). Every PUD set of f::Q^k
into Q^k with the first and second extension properties has an
h_1,...,h_r embedded f:D^k into D^k, 0 in D.

CONJECTURE 2.5. Every instance of Templates 2.1 - 2.4 with order
theoretic is provable in SRP or refutable in RCA_0. Every instance of
Templates 2.1 and 2.3 with piecewise linear is provable in SRP+ or
refutable in RCA_0. Every instance of Templates 2.2 and 2.4 with
piecewise linear is provable in ZF + j:V into V or refutable in RCA_0.

We have only done some preliminary research on this Conjecture. Here's
what we know now.

1. Templates 2.1 - 2.4 with order theoretic reach Con(SRP) over WKL_0, at least.

2. Templates 2.2 and 2.4 with piecewise linear climb through the HUGE
hierarchy, at least.

3. For Template 2.1 with order theoretic, Conjecture 2.5 holds. I.e.,
every instance is provable in SRP or refutable in RCA_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 640th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM

Harvey Friedman