934: Provable Ordinals of Set Theories/1

[Harvey Friedman]

We characterize the provable ordinals of various set theories, including
those with large cardinals. The approach also is a uniform
characterization of the provable ordinals of all theories including the
weak systems that fall under the current state of the art of classical
ordinal notations.

The precise connections between this approach and the existing approach
through ordinal notations has yet to be explored. Perhaps one can in fact
take this new approach and mold it in the image of the ordinal notation
approach and find *new ordinal notation systems for set theories"?

FCN[k,k]

This is the family of functions f:Ak into Ak, where N containedin A
containedin Q.

CTM[k,N]

These are the closed terms defined inductively as follows, using the letter
F that formally represents a function from k-tuples to k-tuples.

1,2,... are (k,k) terms.
If t1,...,tk are (k,k) terms then so are F(t1,...,tk)1, F(t1,...,tk)2, ...,
F(t1,...,tk)k.

It is clear what the value of any term in CTM[k,N] is in any element of
FCN[k,k]. For this, we interpret F(t1,...,tk)i as the i-th coordinate of
F(t1,...,tk).

PROFILE OF FUNCTIONS IN FCN[k,k]
PROFILES OF SUBSETS OF FCN[k,k]

The profile of f in FCN[k,k] is the binary relation on CTM[k,N] given by:

s relates to t if and only if the value of s in f is less than the value of
t in f.

Thus the profile of f s a irreflexive, transitive, connected relation on
CTM[k,N].

Note that the profile of f in FCN[k,k] is a syntactic object that removes
the A's from the picture. In fact, it is clear that if two elements of
FCN[k,k] have an isomorphism which is the identity on N, then they have the
same profile.

The profile of V containedin FCN[k,k] is the intersection of the profiles
of the elements of V.

PROPOSITION. If V containedin FCN[k,k] has at least one well ordered
element (A well ordered under < of Q), then the profile of V is well
founded.

SOME SPECIAL SUBSETS OF FCN[k,k]

We write |x| = max(x).

Let R is an order invariant subset of Q^2k viewed as a relation on Q^k. R
gives rise to the important subset of FCN[k,k] defined as
follows.alpha(R,k) is the set of all f in FCN[k,k] such that the following
holds:

*) For all x in A^k, f(x) is some y = f(y) R x with |y| < |x|, if such y
exists; x otherwise.

Recall gap section SOI and section SOI from
https://cs.nyu.edu/pipermail/fom/2022-May/023281.html

beta(R,k) is the set of all f in alpha(R,k) such that 0,1,... is a gap
section SOI for f, where 0,1,... are left limit points (alternatively, 0 is
a limit point).

gamma(R,k) is the set of all f in alpha(R,k) such that 0,1,... is a section
SOI for f.

THEOREM 1. The ordinals of the profiles of the beta(R,k) have strict sup
the provable ordinal of MAH.

THEOREM 2. The ordinals of the profiles of the gamma(R,k) have strict sup
the provable ordinal of SRP.

FLEXIBILITY

The SOI conditions can be adjusted so that we likewise obtain corresponding
results for a large range of standard fragments of SRP.

TANGIBLE INCOMPLETENESS

We also have another route to Tangible Incompleteness, even simpler than
the above. We can just assert the existence of f:A^k into A^k, A
containedin Q, with condition *) above, and section SOIs of any finite
size. We chose other lead independent statements based on maximality, but
do consider this approach as important and the second line of our Tangible
Incompleteness. I want to make the first line of Tangible Incompleteness as
concise as reasonable, without a lot of alternative options at first.

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

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 934th 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

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220517/9065cbb1/attachment-0001.html>