899: Remarks on Reverse Mathematics/5
Harvey Friedman
hmflogic at gmail.com
Sun Oct 3 12:34:22 EDT 2021
We continue with a discussion of the reverse mathematics of third order objects.
It is now clear how to go about the proper development of RM for
PRESENTED third order objects from the previous posting
https://cs.nyu.edu/pipermail/fom/2021-October/022896.html
We alerted the subscriber that in the case of general third order
objects it is emphatically and totally inappropriate to be introducing
a base theory of higher order functionals, that being totally foreign
to mathematical practice, introducing hidden and totally inappropriate
logical power - whereas RCA0 is so centrally located in so much of
ordinary mathematical practice. Sets of integers are routinely and
pervasively introduced based on comprehension for rather elementary
properties. I have not seen any third order or higher statements used
routinely in mathematics or at all - with any logical strength, even
combined with statements like "no f:R into Z".
So what would a proper RM of third order statements even look like?
One really terrific start is to consider the RM of continuous
functions. Here we take continuous functions as a PRIMITIVE notion.
For those who like the subjects to have a good name, I propose
RM/continuous as a name. That means that RM is being extended by
continuous as a new primitive.
Actually for a really in depth study of this it is best to even go
back and look at the reals themselves. there is a prior subject called
RM/reals. We add reals as primitive. In general, we write RM/a,b,c...
for RM with primistives added for a,b,c,... .
AGENDA
proving the correctness of the RM presentations
RM/reals
RM/reals,(reals)^omega
RM/continuous
RM/REALS
So now we have the usual RCA0 plus a third sort called "reals". What
axioms are appropriate?
1. Axioms for ordered field.
is of course the start. We could stop here as far as base theory is
concerned, but this would be a different subject. It would be
RM/ordered field. But in this limited posting, let's not go there.
Let's continue with RM/reals.
We now have a fork in the road. We can take the view that we always
have finite subsets of ANY sort that we introduce for any purpose. Or
we can introduce another primitive namely an injection j:Z into R. Or
both or whatever. Let's follow a nice good single path here.
So we have the primitive j:Z into R
2. j preserves addition, multiplication, <.
3. The range of j is not bounded above.
4. Every 2^-n (or more elementary, 1/n) Cauchy sequence of rationals
gets arbitrarily close to a real number.
5. Every real number gets arbitrarily close to a Cauchy sequence of rationals.
These axioms prove that the usual treatment of real numbers in RM is correct.
RM/REALS,(REALS)^OMEGA
Infinite sequences of reals are handled in RM with some care. It is
not just a sequence of codes for real numbers. There is an essential
uniformity built in.
We have a sort for infinite sequences of reals, and primitive for the
n-th term. We say that every double sequence of rationals with the
appropriate estimate pointwise converges to an infinite sequence of
reals with appropriate estimate, and every double sequence of
rationals with the appropriate estimate pointwise converges to an
infinite sequence of reals with the appropriate estimates.
This proves that the usual treatment of infinite sequences of real
numbers in RM is correct.
RM/cont
We now treat continuous real function. Best to focus on the ones whose
domain is a product of finitely many intervals in R. The idea is to
state the equivalence of such functions with limits of double
sequences of rational piecewise linear functions, with appropriate
uniform estimates. Then one can prove that the usual neighborhood
condition treatment in RM is correct.
The more general notions of continuity seem to require some additional
thought. One ambitious approach is to simply take the bull by the
horns and introduce a new sort for arbitrary functions from one set of
reals into the reals. Again with composition and restriction axioms.
One has the usual definition of continuity with epsilon delta. But
there seems to be some problems here proving correctness of
neighborhood condition treatments in this generality.
Two extremely important cases of this seem workable. First there is
continuity on open sets in R^n into R^m. In RM, an open set is given
as the union of an infinite sequence of rational open intervals, and
that seems non problematic.Then continuity on open sets also looks to
be non problematic as well.
The second one is continuity on closed sets. Closed sets are non
problematically treated as complements of open sets. Here I have not
thought thru the issues as one is maybe bumping up against the Heine
Borel theorem here and one is always trying to make sure one lands
properly over RCA0 and not more.
I know this is sketchy but hopefully gives an idea as to what kinds of
investigations justify correctness of RM treatments, and also what
kinds of investigations properly investigate the expansion of RM to
third order objects. Of course there is a lot of ideas here that need
perfection.
##########################################
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 899th 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
897: Remarks on Reverse Mathematics/4 10/1/21 1:13AM
898: Ultra Convergence/1
Harvey Friedman
More information about the FOM
mailing list