[FOM] 544: Initial Maximality/HUGE

Fri Sep 12 20:07:48 EDT 2014

*This research was partially supported by the John Templeton
Foundation grant ID #36297. The opinions expressed here are those of
the author and do not necessarily reflect the views of the John
Templeton Foundation.

Using universal properties of sets and partial functions has many
advantages. The disadvantage is that it is less "down to earth" than
squares, roots, and cliques, because it uses propositional
connectives. However, the disadvantage of using propositional
connectives is not nearly as serious as I had thought after talking it
over with a few core mathematicians. After all, propositional
connectives are very familiar in connection with semilinear and
semialgebraic sets, as Boolean combinations. Of course, the
formulations with squares, roots, and cliques will be retained as
important sources of Pi01 that do not involve propositional
connectives.  The current version of #82
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
uses only squares, roots, and cliques.

>From #82 https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
until posting #542
http://www.cs.nyu.edu/pipermail/fom/2014-September/018162.html, we
have always used maximality with respect to inclusion. In #542, we
used t-maximality, which is a weakening of inclusion maximality that
supports finite solutions. In this way, we obtained new explicitly
Pi01 sentences independent of ZFC in #542.

The above works well at the level of SRP. However, for HUGE, we need
something more intense. We had a way to deal with HUGE in #82. but it
didn't fit nicely into the maximality framework. Here we intensify
maximality in a critical way that supports an upgrading of the Pi01
independence from HUGE.

This also allows us to no longer be dependent on the right endpoint,
and so we can work directly in Q^k. For this reason, we will use this
new intensification of maximality also for Pi01 independence from SRP.

The following notation is proving to be very convenient.

DEFINITION 1. f::X into Y if and only if f is a partial function from
X into Y. Let W containedin Q^k. W|<=p = W intersect
(-infinity,p]^k. W|>=p = W intersect [p,infinity)^k. W|J = W intersect
J^k, where J is an interval with endpoints in Q. We apply this
definition to f::Q^k into Q, since we view f as a subset of Q^k+1.
Thus, .e.g., we write f|<=p, which is the result of restricting both
the arguments and values to rationals <= p.

Recall the notion of universal property of f::Q[0,1]^k into Q[0,1]
with (without) constants, that we have been using. See
http://www.cs.nyu.edu/pipermail/fom/2014-September/018161.html
We have also been using this for Q[-n,n] instead of Q[0,1]. We now use
this for Q.

DEFINITION 1. Let X containedin Q and Y containedin Q^k+1. Let A be a
universal property of f::Q^k into Q with constants. A maximal solution
to A is a solution which is not a proper subset of any solution. More
generally, a maximal solution to A in X is a solution from X^k+1 which
is not a proper subset of any solution from X^k+1. Still more
generally, a maximal solution to A in X:Y is a solution f in X which
is not a proper subset of any solution g in X such that f\X = g\X.
Here we view f::Q^k into Q as a subset of Q^k+1.

We start with a failed intensification of maximality which we call
initial maximality*. The * indicates that it is a failure - it is
imply too strong.

DEFINITION 2. Let A be a universal property of f::Q^k into Q with
constants. An initially maximal solution* to A is an f::Q^k into Q
such that for all p in Q, f|<=p is a maximal solution to A in Q|<=p.

THEOREM 1. There is a universal property of f::Q into Q without
constants, with no initially maximal solution*.

We now rescue the initial maximality idea in a very natural way as follows.

DEFINITION 3.  Let X containedin Q^k+1. Let A be a universal property
of partial f:Q^k into Q. An initially maximal solution to A is an
f::E^k into E, 0 in E containedin Q, such that for all p in E, f|<=p
is a maximal solution
to A in E|<=p. More generally, an initially maximal solution to A for
X is an f:E^k into E, 0 in E containedin Q, such that for all p in E,
f|<=p is a maximal solution to A in E|<=p:X.

THEOREM 2. Let 0 in E containedin Q be well ordered. Every universal
property of partial f:Q^k into Q with constants has an initially
maximal solution f::E^k into E. More generally, let X containedin
Q^k+1. Every universal property of partial f:Q^k into Q with constants
has an initially maximal solution f:E^k into E for X.

Of course, Theorem 2 is not concrete. It is Pi12 and not Pi01. It is
included as background material.

PROPOSITION 3. Every universal property of partial f:Q^k into Q
without constants has an initially maximal solution f::E^k into E, N
containedin E, such that f(1,...,k) < 1 implies f(1,...,k) =
f(2,...,k+1).

DEFINITION 4. For x in Q^k, ush(x) is the upper shift of x, which
results from adding 1 to all nonnegative coordinates of x. alpha ==
beta indicates that alpha,beta are both undefined, or alpha,beta are
defined and equal.

PROPOSITION 4. Every universal property of partial f:Q^k into Q
without constants has an initially maximal solution f::E^k into E such
that f(ush(x)) == ush(f(x)).

THEOREM 5. Propositions 3,4 are provably equivalent to Con(SRP) over WKL0.

In fact, Propositions 3,4 can obviously be beautifully templated, and
presumably we can completely analyze these templates - using SRP+ but
not within any consistent fragment of SRP. More specifically,
Proposition 3 can be templated with implications between inequalities
in 1,...,k+1, with complete analysis. Proposition 4 can be templated
using multidimensional liftings of one dimensional piecewise linear
functions. This I can completely analyze. More generally, we can try
to use piecewise linear functions from Q^k into Q^k, and this is a
bigger challenge which I am optimistic about being able to handle.

PROPOSITION 5. Every universal property of partial f:Q^k into Q
without constants has an initially maximal solution f:E^k into E for
Q[1,infinity) such that
i. For all x in Q[1,infinity)^k, f(x+1) == f(x)+1.
ii. For all x in E^k-1, 1 <= min(x) < r-(1/2),  f(r+(1/2),x) = x+1.

THEOREM 7. Proposition 6 is provably equivalent to Con(HUGE) over WKL0.

We now come to the finite forms of Propositions 3,4,6.

DEFINITION 6.   Let A be a universal property of f::Q^k into Q with
constants. A weak initially maximal solution to A is an f::E^k into E,
{0,...,k} containedin E containedin Q, such that for all p in E, f|<=p
is a maximal solution to A in f[{0,...,k}^k]|<=p.

PROPOSITION 8. Every universal property of partial f:Q^k into Q
without constants has a  finite weak initially maximal solution f::E^k
into E such that f(0,...,k-1) < 0 implies f(0,...,k-1) = f(1,...,k).

PROPOSITION 9. Every universal property of partial f:Q^k into Q
without constants has a finite weak initially maximal solution f::E^k
into E such that max(x) <= t implies  f(ush(x)) == ush(f(x)).

PROPOSITION 10. Every universal property of partial f:Q^k into Q
without constants has a finite weak initially maximal solution f:E^k
into E for Q|>=1 such that
i. For all x in Q[1,k]^k, f(x+1) == f(x)+1.
ii. For all x in E^k-1, 1 <= min(x) < r-(1/2),  f(r+(1/2),x) = x+1.

THEOREM 11. Propositions 8.9 are provably equivalent to Con(SRP) over
EFA. Proposition 10 is provably equivalent to Con(HUGE) over EFA>

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

Harvey Friedman