891: Remarks on Reverse Mathematics/1

Sam Sanders sasander at me.com
Thu Sep 23 03:45:10 EDT 2021


Dear Harvey,

> RM is now a neat and clean and clear enough subject to thrive on its own

I agree completely.

> with a fine balance between technical depth and foundational meaning.

I disagree completely, namely as follows:

Here is an old observation:

The FOM archive has plenty of heated discussions about RM versus recursion theory (’99 seems to have been a good vintage).  

A word mentioned a lot in these discussions  is “naturalness”.  These discussions cannot be simplified to 

“recursion theory is somehow unnatural from the pov of mainstream math, and RM is of course natural from this pov"

but this extreme opinion does lurk in the background in that one can almost hear people think it.  


Here is a new observation (or three): 

as shown by myself and Dag Normann the coding in the language of second-order arithmetic is fundamentally defective (if one holds that coding should not change logical strength):

1) even the coding of continuous functions can change the logical strength of basic theorems ([1]), like the Tietze extension thm (an open problem in RM for a while, no less)

2) while the problems in 1) are limited to “a leap in strength from RCA_0 to ACA_0”, the coding of “sligthly” discontinuous function (semi-continuous, bounded variation,..)
can massively change the logical strength of basic thms, like the Jordan decomposition thm.   By “massive”, I mean “all the way up to full SOA versus ACA_0”.  
Paper available on request; the results in [3] are in recursion theory, but translate to RM.  

3) Similar problems exist for countable combinatorics and countable well-orderings:  one needs massive (conventional) comprehension to prove 
basic facts about (third-order) sets of reals that are countable (i.e. there is an injection or bijection to N). This includes Ramsey’s theorem (originally
formulated using sets) and e.g. the very definition of the order type of the rationals ([2]).  



Combining the old and new observations:

grand foundational claims made about RM seem to only hold 

*modulo the use of the coding of objects due to recursion theory*.  

And isn’t this ironic, don’t you think?   

I only see SRM refining this picture, but do prove me wrong.  



Finally, an olive branch:

One could spend a lifetime expanding the previous criticism, and it would be a life
well-spent, but one could also try to find a way of studying third-order arithmetic
via Turing machines (the infinite time variety being unsuitable for these purposes).  

Then, all the people who have spent their lives honing their (second-order) skills can
also prove things about third-order arithmetic.  This is the stage we are at now.  

Best,

Sam

References

[1] Sam Sanders, Representations and the Foundations of Mathematics, to appear in NDJFL, arxiv: https://arxiv.org/abs/1910.07913

[2] Dag Normann and Sam Sanders, On robust theorems due to Bolzano, Weierstrass, and Cantor in Reverse Mathematics, Submitted, https://arxiv.org/abs/2102.04787

[3] ___, Betwixt Turing and Kleene, Submitted, arxiv: https://arxiv.org/abs/2109.01352


> 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