[FOM] 639: Progress in Pi01 Incompleteness 2

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

As promised in http://www.cs.nyu.edu/pipermail/fom/2015-October/019279.html
I start here with 1.

We have been saying that 1) already is "perfectly natural" in a clear
informal sense. It will be of importance to elaborate on this point.

To orient the reader, I 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.

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

My present inclination is to substantially reduce the amount of
material involving maximal roots of order invariant relations on Q^k
(1 above). The Templating is now appearing to be somewhat elusive, as
opposed to the much clearer Templating situation with functions (2,3
above). Everything now has a significantly higher standard of
simplicity. I might change my mind about abbreviating this
relations/roots development as we proceed with 2,3 in later postings.

ORDER INVARIANT RELATIONS AND MAXIMAL ROOTS
by
Harvey M. Friedman
October 27, 2015

1. Roots, Maximality, Sections, Order Invariance
2. Embeddings
3. Graphs, Cliques

1. ROOTS, MAXIMALITY, SECTIONS, ORDER INVARIANCE

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 x,y,z,w for finite tuples
from Q unless indicated otherwise. A relation on a set V is an R
containedin V^2. We write x R y for (x,y) in R. For S containedin Q^k
and p in Q, S|<=p, S|<p, S|>=p, S|>p consist of the x in S where
max(x) is <=p, <p, >=p, >p, respectively. For x,y in Q^k, xy is the
concatenation of x and y, and min(x) is the least coordinate of x.

DEFINITION 1.2. A root of a relation R is a set S such that S^2
containedin R. A maximal root in R is a root of R which is not a
proper subset of any root of R.

We are particularly interested in relations on Q^k. We use two
additional kinds of maximal roots.

DEFINITION 1.3. Let R be relation on Q^k. A nonnegatively maximal root
of R is a root S containedin Q^k|>=0 of R which is not a proper subset
of any root S' containedin Q^k|>=0 of R. A step maximal root of R is
an S containedin Q^k such that for all n >= 0, S|<=n is a maximal root
of R|<=n.

DEFINITION 1.4. Let S containedin Q^k and x in Q^n. The section of S
at x is S[x] = {y in Q^k-n: (x,y) in S}. If n >= k then S[x] =
emptyset.

DEFINITION 1.5. x,y are order equivalent if and only if x,y are of the
same length, and for all 1 <= i,j <= lth(x), x_i < x_j iff y_i < y_j.
E containedin Q^k is order invariant if and only if for all order
equivalent x,y in Q^k, x in E iff y in E.

It is well known that E containedin Q^k is order invariant if and only
if E can be defined as a propositional combination of inequalities
between variables x_1,...,x_k.

PROPOSITION 1.1. Every order invariant relation on Q^k has a maximal
root, where S[0,...,n-1]|<0 = S[1,...,n]|<0.

PROPOSITION 1.2. Every order invariant relation on Q^k has a step
maximal root, where S[0,...,n-1]|<0 = S[1,...,n]|<0.

PROPOSITION 1.3. Every order invariant relation on Q^k has a
nonnegatively maximal root, where S[0,...,n-1]|>n = S[1,...,n]|>n.

The strongest statement of this kind involving sections is as follows.

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).

Propositions 1.1 - 1.4 are implicitly Pi01 via the Goedel Completeness Theorem.

THEOREM 1.5. Propositions 1.2 - 1.4 are provably equivalent to
Con(SRP) over WKL_0. Proposition 1.1 is provable in WKL_0 + Con(SRP).

2. EMBEDDINGS

The set equations in section 1 can be viewed in terms of embeddings.

DEFINITION 2.1. Let S containedin Q^k. h is an embedding of S if and
only if h:Q into Q is partially defined, and for all x,hx in Q^k, x in
S iff hx in S. Here h acts coordinatewise.

DEFINITION 2.2. Let partial h:Q into Q have finite domain. h_* is the
extension of h by the identity strictly below min(dom(h)). h* is the
extension of h by the identity strictly above max(dom(h)). If  h is
empty then we take h_* and h* to be empty.

PROPOSITION 2.1. Let finite partial h:Q into Q be strictly increasing
. Every order invariant relation on Q^k has an h_* embedded maximal
root.

PROPOSITION 2.2. Let finite partial h:Q into Q be strictly increasing.
Every order invariant relation on Q^k has an h_* embedded step maximal
root.

PROPOSITION 2.3. Let finite partial h:Q into Q be strictly increasing.
Every order invariant relation on Q^k has an h* embedded nonnegatively
maximal root.

We also have multiple forms.

PROPOSITION 2.4. Let finite partial h_1,...,h_r:Q into Q be strictly
increasing . Every order invariant relation on Q^k has an
h_1*,...,h_r* embedded maximal root. (Here * is a subscript).

PROPOSITION 2.5. Let finite partial h_1,...,h_r:Q into Q be strictly
increasing. Every order invariant relation on Q^k has an h_1*,...,h_r*
embedded step maximal root. (Here * is a subscript).

PROPOSITION 2.6. Let finite partial h_1,...,h_r:Q into Q be strictly
increasing. Every order invariant relation on Q^k has an h_1*,...,h_r*
embedded nonnegatively maximal root. (Here * is a superscript).

Propositions 2.1 - 2.6 are implicitly Pi01 via the Goedel Completeness Theorem.

THEOREM 2.7. Propositions 2.2, 2.3, 2.5, 2.6 are provably equivalent
to Con(SRP) over WKL_0. Proposition 2.1, 2.4 are provable in WKL_0 +
Con(SRP).

3. GRAPHS, CLIQUES

DEFINITION 3.1. A graph on Q^k is an irreflexive symmetric relation E
on Q^k. A clique in E is an S containedin Q^k such that for all x,y in
S, x E y. A maximal clique in E is a clique in E which is not a proper
subset of any clique in E. An order invariant graph on Q^k is a graph
on Q^k where E is an order invariant relation on Q^k. A nonnegatively
maximal clique in E is a clique in E containedin Q^k|>=0 which is not
a proper subset of any clique in E contained in Q^k|>=0.

THEOREM 3.1. All of the results in sections 1,2 hold with
relations/roots replaced by graphs/cliques.

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

Harvey Friedman