908: Base Theory Proposals for Third Order RM/2

[Harvey Friedman]

1. Third Order RM Compliments RM - no radical foundational advance or
upheaval - here
2. ACA0[3] at level of ACA - experimental - here
3. Some Third Order Reverse Math - RM[3] - next posting
4. Mathematical generation of RCA0[3] - COMBINATORIAL RM[3] - next posting

1. THIRD ORDER RM COMPLIMENTS RM - NO RADICAL FOUNDATIONAL ADVANCE OR UPHEAVAL

I expect properly done foundational third order RM to be an
interesting compliment to existing RM and very closely tied to it. The
logical strengths arising out of third order RM, when done with base
theories properly reflecting the practice of the abstract parts of
mathematical analysis are expected to be normal, and correspond to
what is obtained in RM using appropriately presented third order
objects (presentations being first or second order as usual). This is
what I see in Sander's
https://cs.nyu.edu/pipermail/fom/2021-October/022902.html

An interesting addition to the RM enterprise, but not in any way any
kind of radical foundational advance or radical foundational upheaval
as is suggested by writings and voice recordings by some.

I can imagine a rich range of some relative provability and relative
unprovability results between interesting third order mathematical
statements over appropriate third order base theories,] that are not
simply routine versions of what we normally do in RM with lightfaced
and boldfaced arithmetic presentations.

In particular, I still have not seen any *interesting* reversal
phenomena that one obtains by using unrestricted third order that
isn't closely tied to an ordinary second order RM reversal phenomena
that differs only by using first or second order presentations of the
third order objects in question. When one does such *interesting*
reversals of a third order statement, one builds a second order (or
first order) presentation of a third order object and then does
regular RM to the result.

Of course, this presentation procedure will not work if the third
order statement gains its strength from third order objects with no
reasonable second order presentation. However, then the reversal
concerns statements which gain their power from third order objects
outside the normal realm of objects of mathematical interest, e.g.,
outside Borel measurable third order objects. This is associated with
the reversal being mundane and uninteresting (as far as mathematical
analysis is concerned) such as reversing the mere existence of
characteristic functionals for second or third order quantification.

This pattern I just outlined appears to reflect exactly what is going
on in the results stated in
https://cs.nyu.edu/pipermail/fom/2021-October/022902.html by Sanders.

Nevertheless, I would like to see interesting implications and non
implications between third order statements arising in mathematical
analysis, and also like in usual RM, information arising from the
passage of one third order object to another. Probably the real
interest in third order RM is going to be more along those lines,
rather than anything new about logical strengths not fully reflected
with the usual first and second order presentations in ordinary RM. .

2. ACA0[3] AT LEVEL OF ACA0 - experimental

I am beginning to think of ACA0[3] as a credible and clarifying base
theory for third order RM. Not necessarily the best idea, that remains
to be seen. But a good idea. I think of ACA0[3] as a kind of robust
setup that may readily lend itself to robust investigations into
relative provability of third order statements from abstract analysis.
And obviously for non relative provability, ACA[3] being a bit strong
and robust is an advanage.

So accordingly I give a careful axiomatization of ACA0[3]. Obviously
there is something lost by living on top of ACA0, while it is not yet
clear what a base theory at say the level of RCA0 should be in detail.
But at least there is a well defined project of looking at just how
minimalistic we can be for a third order base theory so that we
actually DERIVE ACA0[3] from the most basic mathematical statements we
can find. And where the boundaries are. This is the point of section 4
in the next posting. And this kind of study discussed in 3 is highly
relevant to the SRM enterprise.

The kind of mathematics being targeted by third order RM can be
roughly described as in these categories from the AMS Classification:

Measure and Integration, Abstract harmonic analysis, Integral
transforms, operational calculus, Functional analysis.

Many of the topics in analysis in that classification scheme are close
enough to computation and continuity, or "essential" continuity, that
third order RM would not be logically relevant, with mathematicians
welcoming the usual RM presentations or already using it themselves.
Things like elaborations on moduli of continuity. That is a main
reason why current RM has not felt compelled to even bring in third
order objects - because presentations are so natural and friendly in
many contexts..

The standard interpretation of ACA0[3] sets the partial functions from
POW(N) into POW(N) to be the arithmetic ones with parameters from
POW(N), which from the descriptive set theory point of view, are just
the partial functions from POW(N) into POW(N) of Baire class < omega,
with domain a set of Baire class < omega. These partial functions are
closed under composition, a very nice thing to have.

ACA0[3] appears to be READY MADE for formalization of order 3
mathematics, with only rather innocent coding apparatus needed. E.g.,
PFCN consists of unary partial functions, and we of course want
partial functions of greater arity, and of general arity n, and even
with infinite arity. Also we may want some of these arguments to be of
sort N instead of sort POW(N). Since we are at the level of ACA0 the
coding apparatus here can be handled basically without thought. Not so
clear if we are working in much weaker third order base theories. And
we are readily prepared to deal with partial functions from R into R
and even on Polish spaces, without worrying about "being a Dedekind
cut" with its universal quantifier, and the like

THE SYSTEM ACA0[3] - details

There are three sorts, N, POW(N), and PFCN. PFCN are the partial
functions from POW(N) into POW(N).

I like to use partial functions here instead of total functions
because let's say we consider even total functions from R into R.
Reals would be Dedekind cuts and not every subset of N or Q is a
Dedekind cut.

Of course, an arguable downside is that one has to be using free
logic. Fortunately there is a very preferred way to do free logic
which I have discussed on FOM several times and written about. I won't
go into that here. Another fortunate thing is that the way ACA0[3]
works, we really don't have to use partial functions but could use
total functions, with default values. This is certainly workable and
should not affect results. Ultimately if the RM community adopts
ACA0[3] as an important base theory, they will decide how they want it
set up. RIght now I recommend partial functions from POW(N) into
POW(N) as the third sort.

We use constant 0 of sort N, unary successor function S from sort N
into sort N, binary functions +,x from sort N into sort N, binary
relation symbol < on sort N, and epsilon between sort N and sort
POW(N).

We have variables n_i, i >= 0, over N, variables x_i, i >= 0, over
POW(N), and variables f_i, i >= 0, over PFCN.

Terms are inductively defined as follows. 0 is a term of sort N. If
s,t are terms of sort N then S(t), s + t, s x t are terms of sort N.
If v is a variable of sort PFCN and t is a term of sort POW(N), then
v(t) is a term of sort POW(N).

Let s,t be terms of sort N. t uparrows, t downarrows, s = t, s wiggle
t, s < t are atomic formulas. This is standard associated with the
proper way to do free logic. uparrows means "undefined". downarrows
means "defined". = means as usual both defined and equal, wiggle means
both sides are either undefined or (defined and equal). s < t means
both sides are defined and s is less than t. As is the right way to do
free logic, a term is defined (downarrows) if and only if all of its
subterms are defined (downarrows). Also variables are automatically
defined.

Let s,t be terms of sort POW(N). t uparrows, t downarrows, s = t, s
wiggle t are atomic formulas.

Let s be a term of sort N and t be a term of sort POW(N). s epsilon t
is an atomic formula.

Let v,w be variables over sort PFCN. v = w is an atomic formula.

Formulas are built up from atomic formulas in the usual way through
connectives and quantification over the three sorts.

A formula is arithmetic if and only if all quantifiers range over N,
and equality between variables of sort PFCN are not allowed. Of
course, free variables of any of the three sorts are allowed in
arithmetic formulas.

AXIOMS
in addition to the standard complete set of logical axioms for free logic

1. Usual quantifier free axioms for 0,S,+,x,<.
2. Induction. Every nonempty object of sort POW(N)  has a < least element.
3. Extensionality. If x,y are of sort POW(N) then x = y if and only if
x,y have the same elements. If f,g are of sort PFCN then f = g if and
only if for all x of sort POW(N), f(x) wiggle f(y).
4. Arithmetic comprehension for POW(N). (therexists x)(forall n)(n
epsilon x iff phi), where phi is any arithmetic formula in which x
does not appear.
5. Arithmetic comprehension for PFCN. (therexists f)(forall x)((f(x)
downarrows iff phi)  and f(x) downarrows implies (forall n)(n in f(x)
iff psi)), where phi,psi are arithmetic formulas in which f does not
appear.

THEOREM 2.1. RCA0[3] proves the same second order sentences as ACA0.
RCA0[3] is finitely axiomatizable.

An interesting problem in RM[3] = third order RM is to obtain
interesting information about the theorems of RM[3]. One can start
with a single third order quantifier, and have many configurations of
numerical and POW(N) quantifiers before and after the single third
order quantifier. Of course, also interesting is AE where the
quantifiers are third order, with various configurations of first and
second order quantifiers there.

##########################################

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 908th 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-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1

Harvey Friedman