944: Inductive Constructions/2

Tue Aug 2 21:55:29 EDT 2022

ENGRAVED IN STONE:

[1] 941: New Stable Maximality/1
https://cs.nyu.edu/pipermail/fom/2022-July/023522.html.

for upcoming Gent Lectures. Also

[2] 942: New Stable Maximality/2
https://cs.nyu.edu/pipermail/fom/2022-July/023523.html

is the most natural direct finite form of [1].

BUT we now give a much better explicitly Pi01 statement based on

UPPERSHIFT INDUCTIVE EMULATOR. UIE. Every relation on Q^k has an
inductive emulator (D,<,S) where S contains ush(S).

from 943: Inductive Constructions/1.

We now define the nondeterministic algorithm ALGUSH takubf infinitely
many steps, but we also consider running it for finitely many steps.

The input is a finite relation R on Q^k. We maintain two objects. The
first is a finite set A
containedin Q^k. The second is a finite sequence x_1,...,x_t from Q^k.
We think of A as the accepted tuples, and the
successive A's form a chain under inclusion. We think of the x's as
the to do list of tuples that need to be processed. That list gets the
first term removed and more tuples are placed at the end.

The goal is for ALGUSH with input R to go on for infinitely many steps, creating
the S in an inductive emulator (D,<,S) where S contains ush(S).

At the beginning of stage 0 (initialization) we see the following.
emptyset, (0,...,0).

At the beginning of stage n >= 0, we have A,x_1,...,x_t, where A is a
finite subset of Q^k, t >= 1, and x_1,...,x_t in Q^k, t >= 1.. We now
process x_1 as follows.

We insert x_1 and ush(x_1) into A; or
We find some y in Q^k, max(y) < max(x_1), such that (x_1,y) is not
order equivalent to any element of R, and insert y and ush(y) into A.

Then we remove x_1 from the list. Finally we refresh. This is done by
listing fld(A' union {x_1,...,x_t})^k in any order and appending this
at the end of x_2,...,x_t. This completes stage n.

NOTE: The alternative treatments of x_1 are called accept or block. Of
course with this refresh there will be a huge number of repetitions,
but for the theory this is not important, and for practical
implementations, we can easily remove repetitions.

REQUIREMENT: We require that for all x,y in A with max(x) < max(y),
that xy is order equivalent to an element of R. If this fails at any
stage then ALGUSH is considered to have failed.

INFINITE ALGUSH. For all finite relations R on Q^k  as input, ALGUSH
can be executed with infinitely many steps.

FINITE ALGUSH. For all finite relations R containedin Q^k as input,
ALGUSH can be executed with any given finite number of steps.

THEOREM 1. INFINITE ALGUSH is provably equivaelnt to Con(SRP) over
WKL_0. FINITE ALGUSH is provably equivalent to Con(SRP) over EFA.

Obviously FINITE ALGUSH is explicitly Pi02. However, it is explicitly Pi01
using the well known algorithm for the first order theory of (Q,<,N).
One can get away with just the quantifier elimination for (Q,<), by
direct estimates placing a bound on the numerators and denominators
needed for the execution.

***HUGE CARINALS***

We modify ALGUSH in the following way We still start with a finite R
containedin Q^2k. But we also specify three pairwise disjoint sets
C,D,Econtainedin Q^k in advance. Thus ALGUSH now depends on R,C,D,E.

At the beginning of stage 0 (initialization) we see the following.
emptyset, (0,...,0).

At the beginning of stage n >= 0, we have A,x_1,...,x_t, where A is a
finite subset of Q^k, t >= 1, and x_1,...,x_t in Q^k, t >= 1.. We now
process x_1 as follows by cases.

case 1. x_1 is in C. Then

We insert x_1 and ush(x_1) into A; or
We find some y in Q^k, max(y) < max(x_1), such that (x_1,y) is not
order equivalent to any element of R, and insert y and ush(y) into A.

case 2. x_1 is in D. Then we insert x_1 and ush(x_1) into A.

case 3. x_1 is in E.

case 4. Otherwise. We either insert x_1 into A or do nothing.

Then we remove x_1 from the list. Finally we refresh. This is done by
listing fld(A' union {x_1,...,x_t})^k in any order and appending this
at the end of x_2,...,x_t. This completes stage n.

REQUIREMENT: We require that for all x in C and y in A with max(x) >
max(y), that xy is order equivalent to an element of R. If this fails
at any stage then ALGUSH is considered to have failed.

We haven't yet worked out good general necessary and/or sufficient
conditions that need to be placed on C,D,E (and possibly on R) for the
executability of ALGUSH. But we have in mind the following choice of
C,D,E.

C = {x in Q^k: x_1 <= ... <= x_k}.
D = {(n-(1/n),p,p+1,...,p+1): 0 <= p <= n-1}, where n >= 2.
E = The set of all (n-(1/n),x) such that n-(1/n) > max(x), not in D.

INFINITE ALGUSH. For all finite relations R on Q^k  as input, ALGUSH
with R,C,D,E can be executed with infinitely many steps.

FINITE ALGUSH. For all finite relations R containedin Q^k as input,
ALGUSH with R,C,D,E can be executed with any given finite number of
steps.

THEOREM 1. INFINITE ALGUSH is provably equivaelnt to Con(HUGE) over
WKL_0. FINITE ALGUSH is provably equivalent to Con(HUGE) over EFA.

Obviously FINITE ALGUSH is explicitly Pi02. However, it is explicitly Pi01
using the well known algorithm for the first order theory of (Q,<,N).
One can get away with just the quantifier elimination for (Q,<), by
direct estimates placing a bound on the numerators and denominators
needed for the execution.

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

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 944th 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-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM
912: Base Theory Proposals for Third Order RM/5  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1  12/11/21  10:15PM
919: Proof Theory of Arithmetic/2  12/11/21  10:17PM
920: Polynomials and PA  1/7/22  4:35PM
921: Polynomials and PA/2  1/9/22  6:57 PM
922: WQO Games  1/10/22 5:32AM
923: Polynomials and PA/3  1/11/22  10:30 PM
924: Polynomials and PA/4  1/13/22  2:02 AM
925: Polynomials and PA/5  2/1/22  9::04PM
926: Polynomials and PA/6  2/1/22 11:20AM
927: Order Invariant Games/1  03/04/22  9:11AM
928: Order Invariant Games/2  03/7/22  4:22AM
929: Physical Infinity/randomness  3/21/22 02:14AM
930: Tangible Indiscernibles/1 05/07/22  7:46PM
931: Tangible Indiscernibles/2 5/14/22  1:34PM
932: Tangible Indiscernibles/3  5/14/22  1:34PM
933: Provable Functions of Set Theories/1 5/16/22  7/11AM
934: Provable Ordinals of Set Theories/1  5/17/22  8:35AM
935: Stable Maximality/Tangible Incompleteness/1  6/3/22  7:05PM
936: Stable Maximality/Tangible Incompleteness/2  6/4/22  11:31PM
937: Logic of Real Numbers/1  6/22/22  7:49AM
938: Logic of Real Functions/1 7/9/22  2:42AM
939: Stable Maximality/1  7/22/22  10:07AM
940: Stable Maximality/2  7/24/2 19:19:48 EDT 2022
941: New Stable Maximality/1  7/29/22  8:44PM
942: New Stable Maximality/2  7/29/22  8:47PM
943: Inductive Constructions/1

Harvey Friedman