[FOM] 638: Rigorous Formalization of Mathematics 2

[Harvey Friedman]

This is a continuation of
http://www.cs.nyu.edu/pipermail/fom/2015-October/019240.html Rigorous
Formalization of Mathematics 1

One aspect of the formalization of mathematics is the underlying
logic, particularly the formulation of and use of free logic.

At the detailed level, there is of course the need for the
formalization of the purely logical part, so that it is adequately
responsive to the great flexibility that mathematicians demand in
their practice.

But before one comes to grip with that requirement, the more general
and more critical strategic issues such as the handling of undefined
terms must be addressed.

There seems to be a small consensus toward the traditional way of
doing free logic as discussed particularly in
http://www.cs.nyu.edu/pipermail/fom/2015-October/019267.html and in
http://www.cs.nyu.edu/pipermail/fom/2015-October/019278.html

Another important issue is that of the number systems N,Z,Q,R,C.

I think that there is an ideal solution to handling this.

1. Recognize at the outset that there is no ideal way of putting
N,Z,Q,R,C into action. There are advantages and disadvantages to
literal versions where we have a chain of actual inclusions, and
everything is a set, and to structural versions where we have systems
that are unique up to isomorphisms and injections, and also some
categorical versions, and hyper categorical versions (don't ask me
what hyper categorical means). I greatly prefer to view Category
Theory as being built on top of set theory, as is the approach, in
essence, in MacClane, Categories for a Working Mathematician.

2. Having recognized 1, the Gold Standard is to take the literal
approach to N,Z,Q,R,C, where we do in fact have a chain of actual
inclusions, and everything is a set.

3. AFTER 2, one can rigorously develop other approaches. E.g., various
structural approaches. Even here, it is not straightforward to sort
them out when it comes to details. E.g., it would appear that one
wants to rely greatly on Existential Instantiation conventions, which
is fine. This facility is of course not needed for the development of
what we call Literal N,Z,Q,R,C.

4. N is defined as the omega of ZFC. Z consists of N together with
some ordered pairs. Q consists of Z together with certain ordered
pairs. R consists of Q together with certain subsets of Q (cuts). C
consists of R together with certain ordered pairs from R.

5. The standard operations are rigorously developed for each of these
number systems as functions, which are sets of ordered pairs.

6. THEN one can develop all kinds of directly useful structural
approaches, and PROVE that various structures and structural items are
isomorphic to what comes out of the Literal development.

7. In general, it may be a good idea to separate Literal developments
from Structural Developments. Literal developments are always offered
as the Gold Standard by which Structural Developments are justified.
E.g., typically all structures obeying certain conditions are
appropriately isomorphic to certain Literal systems previously
developed. It of course follows by transitivity that any two
structures obeying certain conditions are appropriately isomorphic to
each other.

8. Recall in http://www.cs.nyu.edu/pipermail/fom/2015-October/019240.html
 that I am talking about formalization of mathematics, and not
addressing any practical issues surrounding the development of
Provers.

**********************************************************
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 638th 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
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1

Harvey Friedman