938: Logic of Real Functions/1

Sat Jul 9 02:42:07 EDT 2022

Here is a list of fairly recent papers I have placed on my website
concerning RM and SRM.

The Emergence of (Strict) Reverse Mathematics, December 29, 2021, 110
pages, https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/,
#117.

Strict Reverse Mathematics, 6/28/22, 15 pages. This is the second
revised lecture notes for the talk delivered 6/14/22 at the Workshop
on Reverse Mathematics and its Philosophy, June 13-17, 2022, Paris,
France. https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
#79.

Reverse Mathematics, 6/28/22, 22 pages. This is the revised lecture
notes for the talk delivered 6/28/22 at NERODE90, 6/28-6/29.
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
#79, #80.

**************

In this posting and some follow thru postings, I want to talk about a
number of ways of incorporating fairly general notions of real
functions in RM, where we are going to accept the conventional
treatment of real numbers in conventional RM.

I want to begin with a completely semantic approaches that will
definitely provide some guidance for the formal approaches.

NOTEL Real analysis of course includes complex analysis for present purposes..

MODELS OF REAL ANALYSIS

1. The most restrictive models of real analysis that we consider is
that of continuous f:R^n into R^m. Of course, there are a number of
awkward limitations of this model of actual real analysis. For one, we
naturally encounter f whose domain is not all of R^n. The standard
setup in RCA0 is to use Polish spaces, and focus on continuous
functions from one Polish space into another Polish space. But this
does not include, for example, open sets of reals. As I have indicated
elsewhere, the most promising approach to the logic of real functions
(and ultimately of real numbers) is going to be thru SRM, and
precisely for this kind of awkwardness. But that is a topic of another
posting series.

Much less awkward is to take a broader view of f:R^n into R^m. The
idea here is to first focus on the limits of sequences of polynomials
from R^n into R, where such limits will have domains only a subset of
R^n. Then add composition and definition by cases. This gives the
model of the real functions as the real functions in the union of the
Baire classes of finite levels. I.e., write BC(<omega), where BC is
read "baire class".

The obvious objection to this is that it doesn't include everywhere
defined limits of sequences of functions from BC(<omega).

However, the defense is this: where do we get such sequences of
functions from BC(<omega)? It can be argued that in the course of
normal real analysis, as exemplified by looking at lots o publications
and textbooks, one does not get anything like the construction of such
a sequence of functions from BC(<omega).

Or that there is a general description of the kind of analysis that
steers completely clear from the kind of mathematics that yields such
a sequence from BC(<omega).

2. We can also turn this around and try to write down the most
elemental principles that would get us this needed sequence from
BC(<omega).

The best shot at this seems to be introducing indefinite iteration of
f:R^n into R^n by adding a new variable over omega. Some compositional
manipulations needed.

How big a circle around actual real analysis can be put so as to not
include this indefinite iteration idea?

EXPLORATION OF AN EXTENSION OF RM WITH REAL FUNCTIONS

We have the usual RM primitives with reals defined in the usual way.
Actually since we are obviously incorporating ACA0 in this proposal,
we can use extensional reals. I.e., reals as Dedekind cuts. We also
have variables over partially defined real functions of several
variables. We have definition of real functions by composition and
total extensions. We have definition of real functions by sequences of
polynomials, the latter treated in the standard way by RM. This is a
conservative extension of ACA0.

*QUESTION* How much real analysis is comfortably proved in such a
system? What are some basic kinds of real analysis which goes beyond
this?

It seems like we have an interesting extended RM here with this extension.

In the next posting the intention is to look at more abstract
analysis, where we go to even a higher type by looking at a formal
treatment of Borel sets as the least family of sets of sets of reals
satisfying the well known conditions.

The expected result here is in order to get any new significant
strength - say ATR0 - from this, we likely have to perform
manipulations of objects at these higher types that are far from being
reflected in any actual mathematics. But let's actually see what we
can do here in terms of an extended RM.

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

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 938th 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  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM
912: Base Theory Proposals for Third Order RM/5  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1  12/11/21  10:15PM
919: Proof Theory of Arithmetic/2  12/11/21  10:17PM
920: Polynomials and PA  1/7/22  4:35PM
921: Polynomials and PA/2  1/9/22  6:57 PM
922: WQO Games  1/10/22 5:32AM
923: Polynomials and PA/3  1/11/22  10:30 PM
924: Polynomials and PA/4  1/13/22  2:02 AM
925: Polynomials and PA/5  2/1/22  9::04PM
926: Polynomials and PA/6  2/1/22 11:20AM
927: Order Invariant Games/1  03/04/22  9:11AM
928: Order Invariant Games/2  03/7/22  4:22AM
929: Physical Infinity/randomness  3/21/22 02:14AM
930: Tangible Indiscernibles/1 05/07/22  7:46PM
931: Tangible Indiscernibles/2 5/14/22  1:34PM
932: Tangible Indiscernibles/3  5/14/22  1:34PM
933: Provable Functions of Set Theories/1 5/16/22  7/11AM
934: Provable Ordinals of Set Theories/1  5/17/22  8:35AM
935: Stable Maximality/Tangible Incompleteness/1  6/3/22  7:05PM
936: Stable Maximality/Tangible Incompleteness/2  6/4/22  11:31PM
937: Logic of Real Numbers/1

Harvey Friedman