[FOM] 632: Rigorous Formalization of Mathematics 1

[Harvey Friedman]

There has recently been quite a lot of discussion of the important
issue of the approaches in Provers to the underpinnings of basic
mathematics.

The issue has focused somewhat on how the Provers should be handling
the development of the major number systems, natural numbers,
integers, rationals, reals, and complexes. We can even throw in real
algebraics and complex algebraics into the discussion.

It seems that even in 2015, there appears to be advantages and
disadvantages to the various approaches.

Of course, the issue surrounds

i. Do we want literal inclusion of natural numbers in integers in
rationals in reals in complexes? I am completely repulsed by attempts
to address this issue by either throwing out or minimizing the
fundamental importance of or fundamentally altering *identity*. This
is a clear road to absolute disaster, in my opinion. So the issue
remains. Is every natural number a real number? Or do we deliberately
make sure that this does not make any sense? Or that it makes sense in
some altered form? Etcetera.

ii. Or something quite different, e.g. implicit definitions. We can
isolate the properties of the relevant systems as structures, prove
that structures of these various kinds exist and are unique up to
isomorphism, and then use the principle of "working existential
instantiation" to introduce names for examples. So, e.g., Z is the
name for a discrete ordered ring, which is  unique up to isomorphism
if it satisfies the usual condition. And then talk about a more
sophisticated notion of inclusion, that is unique embeddings?

iii. Some variant of the above involving types. I have already said
that I don't like rampant types, but may come to appreciate them if I
am pushed into a corner from which I cannot escape. But not so
quickly.

My main point is that

*the issue of how to give a rigorous convenient official formalization
of mathematics*

has never been adequately addressed even outside the realm of Provers.
And it is of course to be expected that every issue arising without
Provers in mind, is going to be present when one wants to involve
Provers - assuming we want our Provers to be friendly for the 21st
century.

So along these lines, I would like to start at square 1 (or 0?) and
consider just what is the or a best way of rigorously formalizing
mathematics where actual mathematicians are to be the developers, and
disentangle the issue from a myriad of additional issues that are
forced on us by Provers

Furthermore, this "away from Provers" approach would probably benefit
from feedback and surveys of actual working mathematicians. Most
working mathematicians are at least a little bit interested in this
topic since during their teaching careers, they are generally forced
to teach elementary enough mathematics from time to time so that they
have to think a little about this at least in introductory lectures.

Those interested in the rigorous treatment of mathematics, independent
of Provers, could come together and, after feedback and surveys, come
up with a Gold Standard approach and even try to get it endorsed in
some sense by Mathematical Societies. The pitch to the Societies to
get involved would be that this is important in order to lay the
groundwork for future computerizations such as the budding Prover
communities, which do not all adhere to one Gold Standard.

Note the advantage to disentangling this from Provers. The advantage
is that one can start over from scratch on paper, today. (Actually
paper has its advantages.) So

HOW DO WE REALLY WANT TO RIGOROUSLY STATE AND RIGOROUSLY PROVE ACTUAL
THEOREMS AS MATHEMATICIANS? HOW DO WE WANT TO ALL BE ON THE SAME PAGE?

I am envisioning this question to be approached in the usual
semiformal way that mathematicians operate. Of course, when a Gold
Standard emerges that is stated semiformally, and it is time to
incorporate it in some suitable into Provers, that is the time to get
fully formal about it.

**********************************************************
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 632nd 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM

Harvey Friedman