943: Inductive Constructions/1

[Harvey Friedman]

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].

HOWEVER, we have discovered that we can get much simpler explicitly
Pi01 statements and also reach into the HUGE cardinal hierarchy if we
move away from the extremely natural maximality of [1] so the also
natural realm of inductive constructions. Although inductive
constructions are not as prevalent as maximality in mathematics, they
have a definitely important natural place.

DEFINITION 1. An inductive emulator of R containedin Q^2k is a system
(D,<,S), 0 in D containedin Q, S containedin D^k, such that for all x
in D^k, x is in S if and only if for all y in S with max(y) < max(x),
xy is order equivalent to an element of R.

To indicate why we call this an inductive emulator, we offer the following.

THEOREM 1. Let R containedin Q^2k and D containedin Q be well ordered.
There is a unique S containedin D^k such that (D,<,S) is an inductive
emulator of
R containedin Q^2k. Furthermore, this is probably equivalent to ATR0
over RCA0.

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

It is easy to see that we can restrict to finite relations without changing UIE.

THEOREM 2. UIE is provably equivalent to Con(SRP) over WKL0.

***HUGE CARDINALS***

DEFINITION 2. A <=-inductive emulator of R containedin Q^2k is a
system (D,<,S), 0 in D containedin Q, S containedin D^k, such that for
all x in D^k<=, x is in S if and only if for all y in S with max(y) <
max(x), xy is order equivalent to an element of R.

DEFINITION 3. (D,<,S) controls X if and only if X containedin S and
every {x: (p,x) in X and max(x) < p} is some {x: (q,x) in S}.

CONTROLLED UPPERSHIFT INDUCTIVE EMULATOR. CUIE. Every relation on Q^k
has a <=-inductive emulator (D,<,S) which controls ush(S).

It is easy to see that we can restrict to finite relations without
changing CUIE.

THEOREM 3. CUIE is provably equivaelnt to Con(HUGE) over WKL0.

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

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 943rd 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

Harvey Friedman