891: Remarks on Reverse Mathematics/1
Harvey Friedman
hmflogic at gmail.com
Tue Sep 21 00:50:38 EDT 2021
RM is now a neat and clean and clear enough subject to thrive on its
own with a fine balance between technical depth and foundational
meaning.
When I set up RM, I had a more ambitious foundational aim than is
presently realized by RM. This can be seen by the documents leading up
to my RM that are on my webpage under Downloadable Manuscripts. But I
rapidly realized that these more ambitious foundational aims were
premature, and that under some simplifying ideas, the RM subject would
clearly be viable and have that ideal balance between technical depth
and foundational meaning. After several decades, this vision has
definitely taken hold. In fact, work in RM has seemed to accelerate
very rapidly in the last five years.
The original aim that I envisioned is best encapsulated by the moniker
SRM = Strict Reverse Mathematics.
I have written some letters and informal statements about SRM, and
there is one publication on it:
[1] The Inevitability of Logical Strength: strict reverse mathematics,
Logic Colloquium ’06, ASL, ed. Cooper, Geuvers, Pillay, Vaananen,
2009, 373 pages, Cambridge University Press, pp. 135-183.
A copy of [1] is on my website at Downloadable Manuscripts, manuscript
number 58.
The basic idea of SRM is to never use the kind of axiom schemes that
are used throughout traditional f.o.m. (for various purposes). Those
axiom schemes, including my beloved RCA_0, need to be replaced by
fundamental mathematical theorems/facts from the literature, or maybe
simple variants of such. Systems like RCA_0 are shown to be equivaelnt
or derived from such basic mathematical theorems/facts. Thus logical
strength arises organically rather than by fiat from the logician
engaged in schematic formalization.
It is of course not clear from the outset whether such an approach is
even possible or feasible. Hence the title of [1].
The working definition of achieving logical strength rightly used
there is interpreting EFA = exponential function arithmetic.
[1] falls way short of any fully satisfactory treatment of finite SRM.
Here is a plan for a more fully satisfactory treatment of finite SRM.
1. Identify an appropriate language for expressing statements in
finite mathematics. I do not like an open ended series of notions one
after the other. I have at least temporarily fixed on an appropriate
universal language for the expression of finite mathematics. See below
for my current thoughts.
2. Identify a short tower of basic systems logically. Ideally these
are of increasing power under provability and strength. And at this
stage 2, these would be logician's formal systems based on schemes.
The last of these should probably be EFA. I'm leery of using only EFA
because so much important fundamental phenomenon will get lost with
the relatively strong EFA. On the other hand, the simplifying power of
having a few benchmarks here seems compelling.
3. Find fundamental mathematical theorems/facts that are logically
equivalent to each of the levels in 2.
4. Should be able to prove finite Ramsey theorem equivalent to
iterable exponentiation, in a low base theory in 3.
5. Should be to prove various finite forms of Kruskal's theorem are
equivaelnt to the 1-consistency of various formal systems, in a low
base theory in 3.
But in wading through the issues involved in pulling off 1-5 in a
compelling way, I decided once again THIS IS STILL PREMATURE. I had
the right idea in [1] to restrict the language of finite SRM and use
some basic coding that is arguably non problematic.
Ideally, we want a compelling finite SRM to NOT define rationals as
some sort of pairs of integers, but rather introduce rationals as
primitive but with properties of rationals as attached. This can be
done in several ways each of which creates issues that need to be
resolved for finite SRM. One is that the rationals like the integers
are certain sets with certain properties. But the problem with this is
that the relevant sets must be infinite and we already believe that
infinite SRM is a much more delicate matter than finite SRM. The other
approach is the introduction of predicate symbols like "being a
rational" and you have axioms associated with those. But then the
issue arises as to which introduction of predicate symbols is
considered legitimate. Well then this takes us down a very delicate
path because we want to at the same time be minimizing any logical
assumptions and so forth. This is simply PREMATURE right now.
So we have decided that it is best to follow the instincts of [1] that
we should still at least at first have a quite restricted language for
finite SRM. .
So basically we have decided to restrict attention to the further
development of SRM along the restricted lines of [1]. Even with this
restricted language many of the really juicy delicate issues and aims
of finite SRM will be seriously joined.
PRIMITIVES FOR INITIAL FINITE STRICT REVERSE MATHEMATICS
1. Three sorted in free logic as in [1].
2. Three sorts are Integers, Finite Sets of Integers, and Finite
Sequences of Integers. Written Z, FST, FSQ. .
3. We use 0,1,+,-,⋅,exp,<,= on the Z sort. We use epsilon between sort
Z and sort fst.
4. We use val from sort fsq cross sort Z, into sort Z. I.e., the value
of the finite sequence at position n.
5. Exponentiation is binary exponential.
Details are all clear in [1] section 7.
We considered many strictly mathematical statements in this language
of a very fundamental character, and showed equivalences with standard
logical systems that we use in proof theory such as PFA (polynomial
function arithmetic or bounded arithmetic) and EFA (exponential
function arithmetic or ISigma0(exp)).
Here are some research goals.
1. Find more and even find "better" mathematical statements that
achieve this, for PFA, EFA levels, than [1].
2. Do 1 for more levels bounded above by EFA.
3. Do this for level SEFA with finite Ramsey theorem. The hard work
may already be done with 1,2 because one has from 1,2 access to
bounded induction, the critical tool.
4. Treat various finite forms of Kruskal's theorem. These include the
"no elementary recursive sequence" forms. Also the "no primitive
recursive sequence" and the "no recursive sequence" forms. Carefully
analyze how we want to be treating these recursion theoretic functions
in this finite SRM context.
It does seem that deriving bounded induction in a strictly
mathematical way is the heart of the matter here, although working
without EXP here probably opens up some delicate issues.
It may be that we need to drill down hard on just what is needed to
derive bounded induction strictly mathematically and there is a real
challenging subject here of what does or does not suffice.
Remember: exploratory, experimental, some groping in the dark.
A next step beyond this, still in finite SRM, is probably to bring in
polynomials P:Z^n into Z^m as primitive, with a whole new range of
purely mathematical statements and their logical analysis. It is
possible that filtering through Hilbert's 10th inside here could give
us a whole new range of ways of deriving bounded induction from purely
mathematical statements.
##########################################
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 890th 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
Harvey Friedman
More information about the FOM
mailing list