[FOM] 630: Optimal Function Theory 8

[Harvey Friedman]

HAVE JUST STARTED MORE DETAILED CHECKING PROCESS. IN THE MEANTIME...

Continuing from http://www.cs.nyu.edu/pipermail/fom/2015-October/019212.html

In http://www.cs.nyu.edu/pipermail/fom/2015-October/019212.html we
used Universally Define sets of f:Q^k into Q and universally defined
sets of binary operations on {0,...,n!}.

We can instead use Emulations. This has advantages and disadvantages
compared to using the former UD and PUD.

GENERAL PRINCIPLE OF SYMMETRIC EMULATION. Every mathematical object
can be optimally emulated to any given extent, with significant
symmetry.

In our specific context, the use the following notion of emulation.

DEFINITION 1. Let f,g:Q^k into Q^k. g is an r-emulation of f if and
only if every <=r element restriction of g without the value (0,...,0)
is order isomorphic to some restriction of f without the value
(0,...,0). Let R be a relation on the f:Q^k into Q^k. g is an R
maximal r-emulation of f if and only if g is an r-emulation f such
that there is no r-emulation h of f with g R h.

Thus g r-emulates f means "everything small that you see in g
restricted to its support, you already see in f restricted to its
support".

THEOREM 1. Every f:Q^k into Q^k has a <* maximal r-emulation. Every
f:Q^k into Q^k has a <** maximal r-emulation.

PROPOSITION 2. Every f:Q^k into Q^k has a <* maximal r-emulation which
is shift invariant over the positive integers.

PROPOSITION 3. Every f:Q^k into Q^k has a <** maximal r-emulation
which is shift invariant over the positive integers.

In http://www.cs.nyu.edu/pipermail/fom/2015-October/019212.html when I
defined <# I forgot to put the parameter k in. So we write <#k.

PROPOSITION 4. Every f:{0,...,n!}^2 into {0,...,n!} has a <#k maximal
k-emulation without the value (8k)!!-1.

THEOREM 5. Proposition 3 is provably equivalent to Con(SRP) over
WKL_0. Proposition 3 is provable in WKL_0 + Con(SRP).

THEOREM 6. Proposition 4 is provably equivalent to Con(SMAH) over ACA.

Proposition 3 can be seen to be implicitly Pi01 via Goedel's
Completeness Theorem. For some small fixed k, Proposition 3 is
independent of ZFC. As fixed k increases to infinity, Proposition 3
goes up the SRP hierarchy of large cardinals in strength. For fixed k,
Proposition 4 is provable in 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 630th 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  Oct 2 18:23:38 EDT 2015
629: Boolean Algebra/Simplicity

Harvey Friedman