897: Remarks on Reverse Mathematics/4

Fri Oct 1 01:13:36 EDT 2021

We continue with some further remarks concerning the handling of third
order objects in RM and the SRM discipline.

RM has chosen standard coding mechanisms for third order objects with
an eye to having substantive and informative reversals over RCA_0.
Sometimes this is somewhat delicate and awkward to pull off,
particularly in the case of continuous functions from one metric space
into another.

Here is my recommendation. That we consider a range of codings, or
what I call PRESENTATIONS. Then do the usual kind of RM reversals for
fundamental statements under each presentation.

This in fact generates some subareas of RM. Like

1. RM of neighborhood presented continuity, This is the usual branch
of RM focused on the usual way of treating continuous functions.
2. RM of densely presented functions. Here functions from one metric
space into another are presented as a function from a countable dense
subset into a countable dense subset, and the lifting of the function
is defined in the obvious way, resulting in a partial function from
the metric space into the metric space. It would be defined exactly
where all converging sequences to x go to a converging sequence to a
single y..
3. In applicable contexts, use sequences of polynomials with rational
coefficients, the latter presented by the polynomial as a finite
sequence of rationals, via Stone Weierstrass. Or use rational
piecewise linearity. The interaction fo this 3 with 1 above is
important to flesh out.

2 has a great advantage of fundamental simplicity. The usual 1 is
aimed at using RCA0 as the base theory. But 2 seems to naturally be
aimed at using ACA0 as the base theory.

Nevertheless, i expect that all of the delicious RCA0 based RM in
terms of hte usual 1 is preserved when working with 2. That is, one
puts some estimates on the dense presentations in 2 that has the
effect of throwing us into 1.

Now maybe we should back up some and rethink Polish Spaces. And also
separable metric spaces and metric spaces.

The most natural idea, which is of course standard, is to make
countable metric spaces the presentations of Polish spaces.

This doesn't cover non separable metric spaces, but the ones of real
interest seem to have a Polish structure and the actual non separable
metric space is somehow nicely presented from the Polish structure.
This needs to be sorted out properly and systematically.

There are some other important looking kinds of RM here.

4. RM of Baire class alpha. Here 1 <= alpha <= omega_1, with alpha =
omega_1 corresponding to Borel. Here we work with Polish spaces. These
presentations are quite transparent. A presentation is a finite
sequence tree of ordinal alpha with all non terminals having infinite
splitting, and with terminals be assigned presentations of continuous
functions, as in 1,2,3. The assignment is propagated down to the root
transfinitely (or finite sequentially in case alpha is finite).
Particularly important is the case of alpha = 2.

The fundamental idea here is that once one chooses what the
presentations are of the third order objects, one can dive in and
investigate all of the usual third order statements involving, things
like continuity, differentiability, monotonicity, bounded variation,
various integrability, and so forth, and also Lebesgue theory. One
expects to get a normal kind of RM when doing this.

For instance, there has been discussion on FOM of what is called NIN
which is that there is no one-one F:R into Z. Let's look at this from
the lens of the above presentations.

For Baire class omega_1 presentations, we are committed to base theory
ATR0, and NIN is outright provable.

For Baire class 2 presentations, we are committed to base theory ACA0,
and it appears that NIN is provably equivalent to delta-1-1-CA0.

I leave it to the reader to make the calculations for the other
presentation modes discussed above.

ARE THERE ANY ORDINARY MATHEMATICAL THEOREMS INVOLVING THIRD ORDER
OBJECTS WITHOUT PRESENTATIONS THAT HAVE ANY INHERENT LOGICAL STRENGTH?

The examples given thus far attain logical strength only in the
presence of statements about objects that lie way outside of
mathematical practice. This is in sharp contrast with the situation
with ordinary RM. Consider for example this:

NIN. There is no one-one F:POW(N) into N.

Now consider just what additional axioms are needed in order to derive
any logical strength from NIN. Even in the context of say ACA_0.

As far as I can tell, in order to derive any substantial logical
strength from NIN, it is required, at least at present, that one have
some sort of existence principles for functionals of higher types.
Perhaps for full logical strength of the kind suggested, one needs
some sort of existence principles for functions of every finite type.

The use of any functionals of higher type in actual mathematics is
almost nil and certainly is not fundamental like the use of RCA0 which
is pervasive.Obviously higher type functionals is way out of what
normally is called the Borel Universe.

Nevertheless there does remain the challenge of deriving strength from
third order statements like NIN from any fundamental mathematical
principles in pervasive use in mathematics, even at the ontological
level.

I wouldn't rule out the possibility of accomplishing this SRM project
out of hand. But it definitely looks like the right kind of challenge
here and has not even been seriously addressed by any work I have
seen.

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

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

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1:  5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1  5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1  6/19/20 1132PM :
860: Unary Regressive Growth/1  8/120  9:50PM
861: Simplified Axioms for Class Theory  9/16/20  9:17PM
862: Symmetric Semigroups  2/2/21  9:11 PM
863: Structural Mapping Theory/1  2/4/21  11:36PM
864: Structural Mapping Theory/2  2/7/21  1:07AM
865: Structural Mapping Theory/3  2/10/21  11:57PM
866: Structural Mapping Theory/4  2/13/21  12:47AM
867: Structural Mapping Theory/5  2/14/21  11:27PM
868: Structural Mapping Theory/6  2/15/21  9:45PM
869: Structural Proof Theory/1  2/24/21  12:10AM
870: Structural Proof Theory/2  2/28/21  1:18AM
871: Structural Proof Theory/3  2/28/21  9:27PM
872: Structural Proof Theory/4  2/28/21  10:38PM
873: Structural Proof Theory/5  3/1/21  12:58PM
874: Structural Proof Theory/6  3/1/21  6:52PM
875: Structural Proof Theory/7  3/2/21  4:07AM
876: Structural Proof Theory/8  3/2/21  7:27AM
877: Structural Proof Theory/9  3/3/21  7:46PM
878: Structural Proof Theory/10  3/3/21  8:53PM
879: Structural Proof Theory/11  3/4/21  4:22AM
880: Tangible Updates/1  4/15/21 1:46AM
881: Some Logical Thresholds  4/29/21  11:49PM
882: Logical Strength Comparability  5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans  5/16/21 1:29:44
884: Low Strength Zoo/1  5/16/21 1:34:
885: Effective Forms  5/16/21 1:47AM
886: Concerning Natural/1   5/16/21  2:00AM
887: Updated Adventures  9/9/21 9:47AM  2021
888: New(?) kinds of questions  9/9/21 12:32PM
889: Generating r.e. sets  9/12/21  3:38PM
890: Update on Tangible Incompleteness  9/18/21  9:50AM :
891: Remarks on Reverse Mathematics/1  9/21/21  12:50AM   :
892: Remarks on Reverse Mathematics/2  9/21/21  8:37AM :
893: Remarks on Reverse Mathematics/3  9/23/21  10:04PM
894: Update on Tangible Incompleteness/2 9/25/21 2:51AM
895: Provably Recursive Functions and Sigma02  9/27/21  1:21 AM
896: (R,<,0,1,+,-,x,Z)  9/27/21  4:52AM

Harvey Friedman