[FOM] 642: Rigorous Formalization of Mathematics 3

[Harvey Friedman]

We have posted 1,2 in this series:

http://www.cs.nyu.edu/pipermail/fom/2015-October/019240.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019281.html

We have previously discussed

1. Free Logic. I discussed this thoroughly in some postings, and also
see Farmer,

http://www.cs.nyu.edu/pipermail/fom/2015-October/019278.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019294.html

2. N,Z,Q,R,C. I recommended having a Gold Standard with these ordered
under inclusion. I do not recommend using surreals for this purpose
for a number of reasons. Of course, as always, there is no problem
layering anything rigorous on top, as long as you prove along the way
what it's relationship is with the Gold Standard.

Free Logic and what I call the Set Theoretic Infrastructure are more
fundamental and come earlier than N,Z,Q,R,C.

The Set Theoretic Infrastructure incorporates the Logical
Infrastructure, which uses Free Logic. Yes, I am interested in
constructivity, but I don't want to bite off more issues than I can
chew. So I am going to ignore constructivity here, at least for a long
while.

I think that the Set Theoretic Infrastructure must be done just right,
in order to avoid exponential complications down the road.

I want to organize the Logical and Set Theoretic Infrastructure. As I
said repeatedly, it is fine to create your own infrastructure, but it
should reside on top of the Gold Standard Infrastructure.

SET THEORETIC INFRASTRUCTURE = STI
some major features
November 1, 2015

Recall that the sole purpose of STI is to offer a Gold Standard for
supporting convenient, natural, readable rigorous formalization of
mathematics. I envision some empirical tests to see how well STI
succeeds.

I think of STI as stopping with the very convenient presentation of
the axioms of ZFC. Right AFTER STI is the Primary Library = PL. PL
will include such things as N,Z,Q,R,C, but some more. The idea is that
the non logician seriously interested in creating rigorous
mathematical text has all of the tools readily available for doing
this without having to confront matters that require the expertise of
a logician.

There are a lot of components to get STI to be naturally workable, and
these components interact with each other. So it is already a
challenge even to organize the components properly.

First I present a list of major features of STI, some of which are
completely standard, others of which are a bit novel. This is not
comprehensive or detailed enough to be the organization that we seek.

1. Every object is a set. Membership and identity are the primitive
relations. We use epsilon and =.

2. We have Extensionality, Pairing, Union. We use {...} as a k-ary
function symbol for each k >= 1, where {x_1,...,x_k} is defined
necessarily unique set whose elements are exactly x_1,...,x_k.

3. We use <...> as a k-ary function symbol for each k >= 1, where
<x,y> is defined to be {{x},{x,y}}, and <x_1,...,x_k> is defined by
left associativity. Note that 2,3 both involve infinitely many axioms.

4. Every set whatsoever acts as a function of several variables, and a
relation of several variables. Acting like a function of several
variables or a relation of several variables is not something that
requires a special kind of set.

5. We write x(y_1,...,y_k) and x[y_1,...,y_k], for each k >= 1. The
former is the unique z such that <y_1,...,y_k,z> epsilon x. The latter
holds if and only if <y_1,...,y_k> epsilon x.

6. Certain elementary set notation is so basic and convenient that is
part of STI. Emptyset for the empty set. Horseshoe for inclusion ( I
like it with the underline, and without the underline, it means proper
inclusion). Reverse horseshoe also. Pairwise union U. U also used as a
k-ary infix function symbol. Also unary Ux is used for the union,
which is the set of all elements of elements of x. POW(x) for the
power set of x. Here the power set axiom is formulated with horseshoe.
So POW is a unary prefix function symbol. Also boolean ring
operations.

7. Set abstraction. This takes the form {x: phi}, where phi is any
formula. We are of course in Free Logic, so that we do not necessarily
have that {x: phi} is defined. the Free Logic notation uses
i. = means both sides are defined and equal.
ii. ~ means both sides are undefined, or (both sides are defined and equal).
iii. downarrow means defined.
iv. uparrow means undefined.
v. variables are always defined.
vi. Constants always defined? I'm not sure, and see the merit in yes
and no. Tentatively, constants always defined. Of course, this commits
one to proving definedness when introducing new constants by
definition.

Also when introducing function symbols by definition, one has to prove
univalence. However, there is an interesting recommendation I make
concerning the introduction of "associate infix function symbols". But
this is for later, and not for this introductory "some major features"
presentation that are are doing right now.

8. Set abstraction continued. We have the obvious axiom that {x:
phi}downarrow if and only if there is a set whose elements are exactly
those x for which phi (formalized properly). In fact, in an official
form of STI, I would use set abstraction to give the axioms of
pairing, union, power set, separation, replacement.

9. The axiom of choice is stated using the following notation.
Nonempty set uses not= emptyset, with is a line through =, which
should be included in 6. (there exists unique) which is at the Logical
Infrastructure level as a kind of quantifier.

10. Infinity. There is a nonempty set containing the empty set and
closed under x union {x}. Introduce omega by set abstraction, and
since omega is a constant, prove as part of the introduction of omega,
that this exists. Obvious using Separation, which I forgot to say is
{x in y: phi}. At the Logical Infrastructure level, {x in y: phi} is
legitimate notation. One does not have to write, although one could,
{x: x in y and phi}.

11. Relation Abstraction. We want to form the k-ary relation given by
a formula. I don't think that we need, nor do I have in mind, any
special notation for this beyond the obvious use of set abstraction -
in conjunction with Logical Infrastructure. Thus we can write
{<x,y,z>: phi} to refer to a 3-ary relation. We don't have to write
{w: (there exists x,y,z)(w = <x,y,z> and phi}.

12. Function Abstraction. Here the situation is totally different. We
do need special notation for function abstraction. This is something
that mathematicians have been successfully resisting since at least
the invention of the calculus, and Arnon has discussed on the FOM a
number of times. If we are really going to support Fully Rigorous
Formalization then we are going to have to confront this issue of
Function Abstraction properly.

13. In fact, Function Abstraction, properly done, is essentially the
unique place where the Set Theoretic Infrastructure very explicitly
introduces notation that is not in common use in mathematics today.
However, I think that mathematicians will like it very much as a
necessary and convenient component to support rigorous formalization.
It behooves us to make this device as friendly as we can.

In the next posting in this series, I will take up Function
Abstraction notation.

**********************************************************
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 642nd 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  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM

Harvey Friedman