902: Mathematical L and OD/RM

Thu Oct 7 17:13:27 EDT 2021

First a brief response to
https://cs.nyu.edu/pipermail/fom/2021-October/022902.html

*"First a BLANKET CAVEAT: we work over Ulrich Kohlenbach’s base theory
RCA_0^omega, i.e. in higher-order RM from the book RM2001.""Anyone
disagreeing with that framework should FIRST point out which axioms of
RCA_0^omega are problematic and why.  The system RCA_0^omegahas only got
the weakest form of primitive recursion and a weak choice principle needed
to guarantee that RM-codes denote 3rd order objects. "*

This reflects a major misunderstanding of foundational RM. Base theories
for foundational RM are to reflect essential mathematical reasoning, the
more minimalistic in notions and principles the better. That is, confined
to notions and principals that are in constant and pervasive use, a kind of
UNAVOIDABILITY, in the WIDE mathematical terrain at which the foundational
RM is aimed. My RCA_0 is the canonical first version of such a base theory,
which does a very credible - but not perfect - job for this. There is
considerable interest in weakening it - not strengthening it - or even
taking more radical steps such as replacing it with a small number of
actual mathematical statements from the literature, or close variants of
statements from the literature. That is the mission of SRM = strict reverse
mathematics.See paper 58 at
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

What Sanders is talking about can reasonably be called "higher type RM", to
clearly identify that it is a prima facie specialized math logic study and
not meant to have anything like the foundational significance of the usual
RM.

In fact, this "higher type RM" seems more interesting and sensible when
rebranded as "higher type recursion theory" than any kind of specialized RM.

NOTE: There is a typo in
https://cs.nyu.edu/pipermail/fom/2021-October/022903.html I wrote

"I would doubt if any unusual
logical strength (like the higher levels of Z_2) would come out of
basic theorems like NIN and Riemann Integrability, and bounded
variation theorems, when combined with any higher type base theory.
reflecting mathematical practice."

The period after "theory" and before "reflecting" needs to be removed.

I just noticed https://cs.nyu.edu/pipermail/fom/2021-October/022909.html
which continues the same fundamental misundetrstanding of the point of
foundational RM. A base theory is very much NOT supposed to be a system
adequate to formalize some particular mathematics one is concerned with.
Rather a base theory for foundational RM is supposed to be a minimalistic
theory that is inherent in any work down in a wide mathematical terrain. So
right off the bat, any use of what I call 4th and higher order objects
(second order objects are say the reals numbers) for a base theory is prima
facie unsuitable for a base theory.

Now some case can be made for identifying "third order mathematics" and the
need for having some sort of base theory with 3rd order objects present. To
get serious about this, we would have to examine what kind of very weak
third order base theory like principles would be enough to take something
like

NIN. No injective map from pow(N) into N

and derive some interesting logical strength. I would think that any such
third order principles of an acceptable base theory like character would
have at least a usable interpretation in the Borel functions. If that is
the case then NIN adds no strength since NIN is well known to be true in
the Borel functions.

Are there any third order principles that should be included in a base
theory of third order that are not appropriately interpreted by Borel
functions? The answer is no, unless somebody wants to argue otherwise.

NOW ON TO THE MAIN MATERIAL.

1. Mathematical equivalent of V = OD
2. Mathematical equivalent of V = L.
3. Mathematical OD
4. Mathematical L

1. MATHEMATICAL EQUIVALENT OF V = OD

DEFINITION 1.1. An ordinal function is an f:alpha^k into alpha. We identify
them with their graphs which are subsets of alpha^k+1.  x,y in alpha^k are
order equivalent if and only if for all 1 <= i,j <= k, x_i < x_j iff y_i <
y_j. f:alpha^k into alpha is singular if and only if there exists n such
that f is the only f:alpha^k into alpha with the same elements of f^n up to
order equivalence. The sections of f:alpha^k into alpha are obtained by
fixing some i < k arguments to be particular ordinals < alpha.

THEOREM 1.2. (ZF) The following are equivalent.
i. Every ordinal function is a section of a singular ordinal function.
ii. V = OD.

2. MATHEMATICAL EQUIVALENT OF V = L

DEFINITION 2.1. f:alpha^k into alpha is progressively singular if and only
if there exists n such that each g = f|beta, beta <= alpha, is the only
g:beta^k into alpha with the same elements of g^n up to order equivalence.

THEOREM 2.2. (ZF) The following are equivalent.
i. Every ordinal function is a section of a progressively singular ordinal
function.
ii. V = L.

Something special can be done for "every real is constructible".

THEOREM 2.3. (ZF) The following are equivalent.
i. Every countable ordinal function is a section of a singular ordinal
function.
ii. Every countable ordinal function is a section of a progressively
singular ordinal function.
iii. Every real is constructible.

3. MATHEMATICAL OD

THEOREM 3.1. (ZF) The OD ordinal functions are the sections of singular
ordinal functions. The constructible ordinal functions are the sections of
progressively singular ordinal functions. The countable constructible
ordinal functions are the sections of countable singular ordinal functions.

THEOREM 3.2. (ZF) HOD is the least transitive class satisfying KP and
containing as elements, all singular ordinal functions. L is the least
transitive class satisfying KP and containing as elements, all
progressively singular ordinal functions.

We now give a direct mathematical characterization of OD without using
formalisms.

DEFINITION 3.1. x,y in alpha^k are epsilon equivalent if and only if for
all 1 <= i,j <= k, x_i in x_j iff y_i in y_j. f is epsilon singular if and
only if
i. f:A^k into A for some k and transitive A.
ii.There exists n such that f is the unique f:A^k into A with the same
elements of f^n under epsilon equivalence.

THEOREM 3.3. (ZF) OD is the class of ranges of sections of epsilon singular
functions. The constructible subsets of omega are the subsets of omega that
are the range of some countable epsilon singular function.

4. MATHEMATICAL L

DEFINITION 4.1. f is progressively epsilon singular if and only if
i. f:A^k into A for some k and transitive A.
ii.There exists n such that each f|TC(x), x in TC({A}),  is the unique
f:TC(x) into A with the same elements of f^n under epsilon equivalence.

THEOREM 4.1. (ZF) L is the least transitive class satisfying KP and
containing as elements, all progressively epsilon singular functions.

THEOREM 4.2. (ZF) L is the class of ranges of sections of progressively
epsilon singular functions. The constructible subsets of omega are the
subsets of omega that are the range of some countable (progressively)
epsilon singular function.

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

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

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211007/7019e7cc/attachment-0001.html>