[FOM] 633: Constrained Function Theory 1

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

The whole development of Pi01 incompleteness after we introduced
FUNCTIONS needs to be tweaked. There are problems with the forward
directions, which is usually the easy direction. We are busy working
on the situation.

In this posting, we give a new version with partial functions from Q^k
into Q^k which has its advantages, and which has been fairly well
vetted. This is for implicitly Pi01 sentences. However, at the moment,
this new approach is not lending itself nicely to better explicitly
Pi01 sentences. The main reason for moving to functions was to get
better explicitly Pi01 sentences.

Let us review our best implicitly Pi01 sentence BEFORE we moved to functions.

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

Recall that nonnegatively maximal means "maximal among the subsets of Q^k|>=0".

We can of course also use graphs/cliques instead of relations/roots.

We have changed the title of this posting from the previous posting to
have more flexibility in representing the developments.

CONSTRAINED FUNCTION THEORY 1
by
Harvey M. Friedman
October 17, 2015

1. PUD, SHIFT INVARIANCE

DEFINITION 1.1. Q,N,Z+ are the set of all rationals and positive
integers, espectively. We use p,q,x,y,z,w,u,v for rationals, and
a,b,c,d,e,k,n,m,r,s,t for positive integers unless indicated
otherwise.

DEFINITION 1.2. f::Q^k into Q^k indicates that f is a partial function
from Q^k into Q^k. For A containedin Q^k, A <= x if and only if x in
Q^k and for all y in D, max(y) <= max(x).

We now introduce the PUD sets X of f::Q^k into Q^k. PUD is read "purely
universally definable". X should be viewed as a providing a kind of
constraint on f ::Q^k into Q^k. This is a
standard notion from elementary model theory, which should also be
familiar to many in combinatorics, certain parts of algebra, real
algebraic/analytic geometry, and computer science.

CONJECTURE. For any mathematician and theoretical computer scientist,
there is a presentation of PUD that is friendly for them.

DEFINITION 1.3. X is a PUD set of f::Q^k into Q^k if and only if X can be
defined in the following form. The set of all f::Q^k into Q^k such that
(forall x_1,...,x_m in Q)(if all terms in phi are defined then phi
holds), where phi is a propositional combination of inequalities s <
t, where s,t are either x's or coordinate functions f_i applied to x's.

Obviously the empty function must be an element of X.

DEFINITION 1.4. Let f::Q^k into Q^k. f is negatively shift invariant
over N if and only if N^k containedin dom(f), and for all x in N^k,
max(f(x)) < 0 implies f(x) = f(x+1).

Here x+1 is the result of adding 1 to all coordinates of x.

2. EXTENDABILITY

We seek a sufficient condition for a PUD set of f::Q^k into Q^k to
have a (good) element which is negatively shift invariant over N.

DEFINITION 2.1. Let X be a set of f::Q^k into Q^k. X has upper
extendability if and only if for all f in X and dom(f) <= x, some f
union (x,y) lies in X.

THEOREM 2.1. Upper extendability for PUD sets of f::Q^k into Q^k is
recursively enumerable.

This is by Goedel's Completeness Theorem.

PROPOSITION 2.2. Every upper extendable PUD set of f::Q^k into Q^k has
a g:D^k into Q^k negatively shift invariant over N.

It can be seen that Proposition 2.2 is implicitly Pi01 via Goedel's
Completeness Theorem.

THEOREM 2.3. Proposition 2.2 is provably equivalent to Con(SRP) over
WKL_0. Proposition 2.3 is independent of ZFC for some small k
(assuming Con(SRP)). These results hold even if we restrict ourselves
entirely to f::Q^k into Q^k that are delta-0-2 in the sense of
recursion theory.

SRP is ZFC + {there exists a limit ordinal with the k-stationay Ramsey
property}_k. SRP+ = ZFC + (forall n)(therexists a limit ordinal with
the k-stationary Ramsey property).

NOTE: This is the same if we use k-subtle or k-ineffable.

**********************************************************
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 633rd 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

Harvey Friedman