902: Mathematical L and OD/RM

[Mikhail Katz]

Hi Sam,
Thanks for this summary.  I gather that there may be two approaches to RM,
say (A) and (B), with a certain philosophical difference between them.  The
difference concerns the attitude toward Kohlenbach's system RCA_0^\om.
Here track A rejects RCA_0^\om as of foundational significance for RM,
whereas track B accepts it.  One central philosophical disagreement
concerns the attitude toward certain 4th order objects, but as you point
out the disagreement concerns certain 3rd-order systems as well.  The issue
seems to be that such objects cause "explosions" and/or the phenomenon that
the behavior of certain basic mathematical entities diverges from the
behavior of their codes within RM, in that the truth value of certain
classical mathematical assertions changes depending on whether one
interprets them as referring to the mathematical entity or its code within
RM.
There is probably a zillion inaccuracies in what I wrote (and I would be
happy to be corrected) but my point is that if the discussion were
presented in such non-technical terms, it would be accessible to a broader
audience of interested mathematicians (not to speak of historians or
philosophers).
I can't help thinking of the historical parallel of Brouwer's dismissive
reaction to Heyting's formalisation of Brouwer's intuitionism, but as
history showed, Brouwer doesn't own Intuitionism.
Best,
Misha Katz

On Thu, Oct 14, 2021 at 2:08 AM Sam Sanders <sasander at me.com> wrote:

> Dear FOM,
>
> > What Sanders is talking about can reasonably be called "higher type RM",
>
> Indeed, especially since Ulrich Kohlenbach has called it “higher order RM”
> (also the name of his RM2001 paper), a name I have used ad nauseam, the FOM
> would agree.
>
> > to clearly identify that it is a prima facie specialised math logic
> study and not meant to have anything like the foundational significance of
> the usual RM.
>
> Ulrich’s higher-order RM is however mentioned by Montalban in the “open
> questions in RM” paper published around 2011 in the BSL.
>
> Why the sudden reaction now after 10 years?
>
> >  So right off the bat, any use of what I call 4th and higher order
> objects (second order objects are say the reals numbers) for a base theory
> is prima facie unsuitable for a base theory.
>
> Here is where we disagree: 4th order objects and higher are just around in
> higher-order RM with the weakest possible axioms governing them (projection
> and application), as discussed at length / ad nauseam my previous email.
> What is wrong with having the language around with the most basic
> constructs governing this language?
>
> But let us go along with Harvey Friedman, not in the least because
> everything I have said also works if we “saw off” the type level at
> third-order objects, as follows.
>
> To be absolutely clear: take Kohlenbach's RCA_0^omega and remove all
> mention of fourth-order and higher in the language and axioms.  Let the
> resulting system
> be known as RCA_0^3, presumably very similar to Noah Schweber’s system.
>
> There are two points to be made here:
>
> 1) the explosions from my previous email(s) still go through, and we will
> revisit a particularly conceptual one,
>
> 2) natural models of subsystems of third-order arithmetic satisfying Z_2
> still falsify NIN (there is no injection from 2^N to N).
>
>
> > Now some case can be made for identifying "third order mathematics" and
> the need for having some sort of base theory with 3rd order objects present.
>
> See RCA_0^3 above.
>
> The “explosions” I have mentioned still go through at this level.  For
> instance, both a) and b) in isolation do not go beyond ACA_0 when combined
> with RCA_0^3, while the combination a) + b) proves ATR_0.
>
> a) The Jordan decomposition theorem: a function of bounded variation on
> [0,1] can be written as the difference of two monotone functions
>
> b) The sign function on R exists (or any discontinuous function on R).
>
> Moreover, combining a) with the Suslin functional (i.e. higher-order
> Pi_1^1-CA_0), we obtain Pi_2^1-CA_0.
>
> The Suslin functional is the third-order object that decides
> Pi_1^1-formulas (in Kleene normal form).  RCA_0^3 plus the Suslin functional
> is Pi_3^1-conservative over Pi_1^1-CA_0.
>
> > To get serious about this, we would have to examine what kind of very
> weak third order base theory like principles would be enough to take
> something like
> >
> > NIN. No injective map from pow(N) into N
> >
> > and derive some interesting logical strength.
>
> To the best of my knowledge, one cannot derive any strength from NIN (for
> rather technical reasons).
>
> However, NIN is still hard to prove as follows.  Let us start with the
> observation that many
> natural models of SOSOA (called REC, ARITH, HYP, …) are based on (Turing)
> computability theoretic
> classes.  Let us now build a natural model of a subsystem of third-order
> arithmetic that satisfies Z_2,
> based on the canonical higher-order extension of Turing machines, namely
> Kleene’s S1-S9.
>
> Let S_k^2 be the third-order functional that decides Pi_k^1-formulas (in
> their Kleene normal form).
> Let RCA_0^3 be as above and define Z_2^3 as RCA_0^3 plus the union of all
> S_k^2.  As noted
> previously, the system Z_2^3 is a conservative extension of Z_2.
>
> To build the “canonical” model M of Z_2^3, take all objects of order at
> most three computable (S1-S9)
> in some S_k^2.  Then for each element f of Cantor space in M, we can
> assign a unique/least natural e
> such that  “e is the code for an S1-S9 algorithm to compute f from some
> S_k^2”.
>
> Let F be a mapping that to each f of Cantor space in M assigns such e.
> Clearly such F exists by the Axiom of
> Choice.  By Robin Gandy’s “selection principle”  (called “Gandy
> selection”), the model M already contains
> such F.  Clearly, the latter is an injection from 2^N to N (from the pov
> of M).
>
> Hence, a most natural model of Z_2^3 satisfies the negation of NIN, making
> the latter hard to prove (in terms of conventional comprehension).
>
> > I would think that any such third order principles of an acceptable base
> theory like character would have at least a usable interpretation in the
> Borel functions. If that is the case then NIN adds no strength since NIN is
> well known to be true in the Borel functions.
>
> For representations of Borel functions, this would be correct. For “raw”
> third-order objects that happen to be Borel, not so much:
>
> As noted in previous emails, NIN is equivalent (also over RCA_0^3) to
> versions of NIN for functions R-> Q of bounded variation, Borel functions,
> semi-continuous functions…
>
> Best,
>
> Sam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211014/5c0ca7b8/attachment-0001.html>