892: Remarks on Reverse Mathematics/2
Harvey Friedman
hmflogic at gmail.com
Tue Sep 21 08:37:41 EDT 2021
In this posting I want to focus on how to handle third order objects in RM.
But BEFORE we discuss this, I had some further thoughts on FSRM =
finite strict reverse mathematics.
A. This should be intensively investigated on its own, independently
of, even separately from, and to a large extent before, SRM = Infinite
SRM.
B. At least for a while, we should allow only a growing but relatively
small list of primitives before jumping into the situation with
general open ended primitives. The general open ended primitives for
FSRM is ultimately very much wanted, but we regard that as premature,
recommending it wait for a deeper development with limited primitives.
C. Here are the recommended primitives we envision. i - iv are
already used in reference [1] in posting #891.
i. language of discrete ordered rings, for handling integers.
ii. binary exponentiation with nonnegative base and exponent.
iii. finite sets of integers with epsilon.
iv. finite sequences of integers with valuation (val).
v. field of rationals, with various new primitives. Including mapping
from Q into Z^2 via reduced forms. finite sets of rationals, finite
sequences of rationals, membership, and valuation (val).
vi. polynomials from Q^n to Q^m, with various new primitives. Ring
operations on polynomials. Evaluation of polynomials.
vii. field of complex integers, with various new primitives. finite
sets, finite sequences, and field of complex rationals.
viii. ordered field of real algebraic numbers. field of complex
algebraic numbers. Lots of new primitives.
ix. extensions of exponentiation ultimately to complex algebraic
numbers, and associated infinite series expansions.
x. finite trees and other finite combinatorial objects, with liberal
new primitives.
I anticipate an incredibly delicious and deep complex of derivations
of bounded and higher inductions form purely fundamental mathematical
theorems/facts. Reference [1] only a modest beginning.
HANDLING THIRD ORDER OBJECTS IN REVERSE MATHEMATICS
Third order objects arise in RM most commonly when dealing with F:R
into R. More generally, R can be a Polish space.
Here are several ways to go about this.
1. Require them to be continuous or piecewise continuous and use
coding by neighborhood conditions. This is the standard way that third
order objects are now dealt with in RM. Base theory RCA_0.
2. Treat them as another sort not tied to second order objects. I.e.,
in terms of some sort of third order RM.
3. Treat them as Baire class 2 functions. These are treated as
explicitly Baire class 2 meaning that one has a double sequence of
continuous functions given as in 1. Base theory ACA_0.
4. It is natural to consider Baire class n functions, n >= 1, in
method 3. Base theory ACA_0 and ACA' for Baire class n's all at once.
ACA' is for all n the n-th Turing jump of any set exists.
5. Treat them as Borel functions with the usual Borel coding scheme
for basically Baire class alpha, a countable ordinal. Base theory
ATR_0.
IMPORTANT POINT: 3,4,5 can be presented WITHOUT using continuous
functions. Instead one can use trivial non problematic functions with
even rational data. So any issues with the coding of continuous
functions and the coding of sequences of continuous functions can be
bypassed for 3,4,5. This also suggests the use of sequences of finite
objects to present continuous functions in 1.
I regard 2 as a problematic idea, unless one bears down and seriously
uses the SRM perspective - see posting #891. The vast bulk of third
order mathematical constructions are based on fundamentally sequential
processes. That does allow for discontinuous objects. Baire class 2 is
a tremendously large family of third order objects given by sequential
processes.
Now look at the following sample of third order statements through the
lense of 1,3,4,5. This stays within the existing RM framework. Each of
these third order statements is treated in these four ways, resulting
in four statements. What is their reverse math?
There has been enough of an explosion of work in RM lately that
perhaps a large amount of this has been done.
A. Every sequence from X misses an element of X. Here X is a Polish
space (with an appropriate nontriviality condition).
B. No function from X into Y is injective. Here X is a nontrivial
Polish space and Y is an appropriately countable space.
C. No function from X into Y is bijective. Here X is a nontrivial
Polish space and Y is an appropriately countable space, but even wider
contexts may be very interesting.
D. Every monotone function has at most countably many discontinuities.
Here use R but maybe some other ordered spaces.
E. Every function of bounded variation is the difference between two
monotone functions.
F. A function is Riemann integrable if and only if it is continuous
almost everywhere.
G. A monotone function is differentiable almost everywhere.
H. The union of a sequence of sets of measure zero is of measure 0.
I. Countable additivity of Lebesgue measure.
So the idea is to admit right off that there are different "brands''
of third order functions in RM and see how standard third order
statements fare under the various brands.These brands can be stated in
fairly robust ways.
##########################################
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 892nd 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 2:38PM
890: Update on Tangible Incompleteness 9/18/21 9:50AM
891: Remarks on Reverse Mathematics/1
Harvey Friedman
More information about the FOM
mailing list