[FOM] 612: Binary Operation Emulation and Continuation 1

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

We now prefer to be extending BOPS = binary operations. Again, these
are partial, and thus to be viewed as a set of ordered triples.

More specifically, we will be emulating and continuing finite BOPS. A
finite BOP can actually be displayed as a "multiplication table" in
the usual way we were taught in school - except some of the entries
are left BLANK.

We will now be back to having a more or less unconditional equation as
the punch line. We exploit the very familiar idea of multiple products
in a bop, *. E.g.,

c*((a*b)*c)

is a length 4 product.

NOTE: There is the possibility of using only associative bops, but we
won't pursue this in this posting. The advantage of associative bops
is that there is no longer any need for parentheses.

The key advantage to bops is the natural notion of calibrated
generation. We use the notation

*[a_1,...,a_k]
*[k; b_1,...,b_n]

for the set of all products of the a's or b's of length at most k.

So we arrive at the simple single parameter statements:

PROPOSITION 1.1. Every finite * in Q has a maximal k-emulation ** in
Q|>=0, where **[0,...,k-1] = **[1,...,k] above k.

PROPOSITION 1.2. Every finite * in Q|>k has a maximal k-continuation
** in Q|>=0, where **[0,...,k-1] = **[1,...,k] above k.

where all of the definitions will be given in full detail below.

For the explicitly Pi01 forms, we again use 1!,...,n! , where we need
two parameters, k,n. We have to take the set of all length <=k
products from 1!,...,n!. I cannot resist making the implicitly Pi01
forms as spectacularly simple as I can, and so do not want to risk
cluttering it up with more parameters than are needed. But with this
approach to the explicitly Pi01 forms, which has the punch line

has a blah blah blah which omits (8k)!!-1

I will definitely need two parameters. So I add the second parameter gently, as

**[k; a_1,...,a_n]

which is the set of products of the a's of length at most k.

The biggest payoff for moving from sets to functions to bops comes
with the definition of factorial maximality.

1. BOPS IN Q

DEFINITION 1.1. Q,Z,N,Z+ is the set of all rationals, integers,
nonnegative integers, and positive integers, respectively.
n,m,r,s,t,i,j denote positive integers and p,q denote rationals unless
otherwise indicated. x,y in Q^k are order equivalent if and only if
for all 1 <= i,j <= k, x_i < x_j iff y_i < y_j..A,B containedin Q are
equal above p if and only if they contain the same elements > p.

DEFINITION 1.2. Let E containedin Q and p in Q.  E|>p,
E|>=p, E|<p, E|<=p consists of the elements of E that are >p, >=p, <p,
<=p, respectively. * is a
bop in X if and only if * is a partial binary function from X into X.
Bops are treated as subsets of X^3.

DEFINITION 1.3. Let * be a bop in Q and X containedin Q. A
k-emulation of * in X is a bop ** in X such that the following
holds. For any x_1,...,x_k in ** there exists y_1,...,y_k in * such
that the two concatenations x_1...x_k and y_1...y_k are
order equivalent. A maximal k-emulation of * in X is a k-emulation of *
in X which is not a proper subset of any k-emulation of * in X.

DEFINITION 1.4. Let * be a bop in Q and X containedin Q. A
k-continuation of * in X is an emulation of * in X which contains *. A
k-maximal continuation of * in X is a continuation of * in X which is not a
proper subset of any k-continuation of * in X.

DEFINITION 1.5. Let * be a bop in X. *[a_1,...,a_k] is the set of all
defined * products of a's of length at most k. *[k; b_1,...,b_n] is
the set of all defined * products of b'x of length at most k.

* and ** always refer to bops.

PROPOSITION 1.1. Every finite * in Q has a maximal k-emulation ** in
Q|>=0, where **[0,...,k-1] = **[1,...,k] above k..

PROPOSITION 1.2. Every finite * in Q|>k has a maximal k-continuation
** in Q|>=0, where **[0,...,k-1] = **[1,...,k] above k..

We now use step maximality in Q.

DEFINITION 1.6. Let * be a bop in Q. A step maximal k-emulation of *
in Q is a bop ** in Q where each *|<=n, n in N, is a
maximal k-emulation of f in Q|<=n. A step maximal k-continuation of *
in Q is a  bop ** in Q where each **|<=n is a
step maximal continuation of * in Q|<=n.

PROPOSITION 1.3. Every finite * in Q has a step maximal k-emulation **
in Q, where **[0,...,k-1] = **[1,...,k] below 0.

PROPOSITION 1.4. Every finite * in Q|<0 has a step maximal
k-continuation ** in Q, where **[0,...,k-1] = **[1,...,k] below 0.

THEOREM 1.5. Propositions 1.1 - 1.4 are provably equivalent to Con(SRP)
over WKL_0.

Propositions 1-4 are implicitly Pi01 via Goedel's Completeness Theorem.

There is another interesting BONUS for going to BOPS. Some of this
bonus can be done with the earlier formulations, but there is one
aspect that is BEST with BOPS.

THEOREM 1.6. There is a fixed finite * in Q|<0 and fixed k such that
Propositions 1.1,1.3,1.4 are provably equivalent to Con(SRP) over
WKL_0. There is a fixed k and fixed finite * in Q|>k such that
Proposition 1.2 is provably equivalent to Con(SRP) over WKL_0.

So what? Well, it appears that we can take * and k both to be quite
small. How small is somewhat difficult for me to wrap my head around
as things are so new.

Now here is the plan.

Firstly, to fix k to be something like 8, or maybe even 4. .

Then to fix * to be WRITABLE as an actual modest sized TABLE. Recall
that bops have obvious displayable MULTIPLICATION TABLES.

It will be easier to work with emulations rather than continuations
here. And I don't yet have a feel for the size of the required table.

2. BOPS IN {1,...,n!}

DEFINITION 2.1. Let * be a bop in {1,...,n!}. A factorial maximal
k-emulation of * in {1,...,n!} is a k-emulation ** in {1,...,n!},
where all k-emulations of * in
{1,...,n!} extending * have **[k;1!,2!,...,n!] = *[k; 1!,2!,...,n!]. A
strong factorial maximal k-emulation of * in {1,...,n!} is a
k-emulation ** in {1,...,n!}, where all k-emulations of ** in
{1,...,s!} extending *|<=s! have **[k;1!,2!,...,s!] = *[k;
1!,2!,...,s!]., 1 <= s <= n.

PROPOSITION 2.1. Every * in {1,...,n!} has a factorial maximal
k-emulation in {1,...,n!}^k that omits (8k)!!-1.

PROPOSITION 2.2. Every * in {1,...,n!} has a strong factorial maximal
k-emulation in {1,...,n!}^k that omits (8k)!!-1.

These Propositions are obviously explicitly Pi01.

THEOREM 2.3. Propositions 2.1 and 2.2 are provably equivalent to
Con(SMAH) over ACA.

3. TEMPLATE

It is most convenient to focus on

PROPOSITION 1.1. Every finite * in Q has a maximal k-emulation ** in
Q|>=0, where **[0,...,k-1] = **[1,...,k] above k.

Now here is the main point. The punch line

**[0,...,k-1] = **[1,...,k] above k

can be viewed as asserting a Boolean relation among the following sets:

The intervals contained in Q with endpoints from the extended rationals.
The k-generated sets.

Here the k-generated sets are the sets of the form **[p_1,...,p_k],
p_1,...,p_k in Q.

We call the latter sets the k-generated sets.

TEMPLATE 3.1. Let phi be a Boolean relation between the rational
intervals and the k-generated sets of a bop. Every * in
Q has a maximal k-emulation ** in Q|>=0 satisfying phi.

Note that every instance of Template 3.1 is implicitly Pi01 via
Goedel's Completeness Theorem.

We already know that there are instances of Template 3.1 that are
provably equivalent to Con(SRP) over WKL_0.

CONJECTURE. Every instance of Template 3.1 is provable or refutable in
WKL_0 + Con(SRP).

I will first try to exploit the structure of the phi that we use, to
obtain significant partial results. The phi that we use for large
cardinal power is a Boolean involving only two k-generated sets and
only one rational interval. We expect no difficulties in handling
these, no matter what fixed k we use. If k is not too small, then many
of these will result in equivalence with Con(SRP).

************************************************************
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 6112h 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

Harvey Friedman